---

Definition: poset_sig
PosetSig ==  car:Type × eq:car ⟶ car ⟶ 𝔹 × (car ⟶ car ⟶ 𝔹)

Lemma: poset_sig_wf
PosetSig ∈ 𝕌'

Definition: set_car
|p| ==  fst(p)

Lemma: set_car_wf
∀[p:PosetSig]. (|p| ∈ Type)

Definition: set_eq
=b ==  fst(snd(p))

Lemma: set_eq_wf
∀[p:PosetSig]. (=b ∈ |p| ⟶ |p| ⟶ 𝔹)

Definition: set_le
≤b ==  snd(snd(p))

Lemma: set_le_wf
∀[p:PosetSig]. (≤b ∈ |p| ⟶ |p| ⟶ 𝔹)

Lemma: subtype_rel_poset
PosetSig ⊆r PosetSig{[i | j]}

Lemma: poset_sig_inc
PosetSig ⊆r PosetSig{[i | j]}

Definition: dset
DSet ==  {s:PosetSig| IsEqFun(|s|;=b)} 

Lemma: dset_wf
DSet ∈ 𝕌'

Lemma: dset_properties
∀[s:DSet]. IsEqFun(|s|;=b)

Lemma: assert_of_dset_eq
∀[s:DSet]. ∀[a,b:|s|].  uiff(↑(a (=b) b);a = b ∈ |s|)

Lemma: decidable__dset_eq
∀s:DSet. ∀a,b:|s|.  Dec(a = b ∈ |s|)

Lemma: dset_eq_refl
∀[s:DSet]. ∀[a:|s|].  a (=b) a = tt

Definition: mk_dset
mk_dset(T, eq) ==  <T, eq, eq>

Lemma: mk_dset_wf
∀[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].  mk_dset(T, eq) ∈ DSet supposing IsEqFun(T;eq)

Definition: set_leq
a ≤ b ==  ↑(a (≤b) b)

Lemma: set_leq_wf
∀[p:PosetSig]. ∀[a,b:|p|].  (a ≤ b ∈ ℙ)

Lemma: decidable__set_leq
∀p:PosetSig. ∀a,b:|p|.  Dec(a ≤ b)

Lemma: assert_of_set_leq
∀[p:PosetSig]. ∀[a,b:|p|].  uiff(↑(a (≤b) b);a ≤ b)

Definition: set_blt
a <b b ==  (a (≤b) b) ∧b (¬b(b (≤b) a))

Lemma: set_blt_wf
∀[p:PosetSig]. ∀[a,b:|p|].  (a <b b ∈ 𝔹)

Lemma: comb_for_set_blt_wf
λp,a,b,z. (a <b b) ∈ p:PosetSig ⟶ a:|p| ⟶ b:|p| ⟶ (↓True) ⟶ 𝔹

Definition: set_lt
a <p b ==  ↑(a <b b)

Lemma: set_lt_wf
∀[p:PosetSig]. ∀[a,b:|p|].  (a <p b ∈ ℙ)

Lemma: set_lt_is_sp_of_leq
∀[p:PosetSig]. ∀[a,b:|p|].  uiff(a <p b;strict_part(x,y.x ≤ y;a;b))

Lemma: set_lt_is_sp_of_leq_a
∀[p:PosetSig]. ∀[a,b:|p|].  uiff(a <p b;(a ≤ b) ∧ (¬(b ≤ a)))

Lemma: decidable__set_lt
∀p:PosetSig. ∀a,b:|p|.  Dec(a <p b)

Lemma: assert_of_set_lt
∀[p:PosetSig]. ∀[a,b:|p|].  uiff(↑(a <b b);a <p b)

Definition: qoset
QOSet ==  {s:DSet| UniformPreorder(|s|;a,b.a ≤ b)} 

Lemma: qoset_wf
QOSet ∈ 𝕌'

Lemma: qoset_subtype_dset
QOSet ⊆r DSet

Lemma: qoset_properties
∀[s:QOSet]. UniformPreorder(|s|;a,b.a ≤ b)

Lemma: qoset_refl
∀[s:QOSet]. ∀[a:|s|].  (a ≤ a)

Lemma: set_leq_weakening_eq
∀[s:QOSet]. ∀[a,b:|s|].  a ≤ b supposing a = b ∈ |s|

Lemma: qoset_trans
∀[s:QOSet]. ∀[a,b,c:|s|].  (a ≤ c) supposing ((b ≤ c) and (a ≤ b))

Lemma: set_leq_transitivity
∀[s:QOSet]. ∀[a,b,c:|s|].  (a ≤ c) supposing ((b ≤ c) and (a ≤ b))

Lemma: set_leq_trans
∀[s:QOSet]. UniformlyTrans(|s|;x,y.x ≤ y)

Lemma: qoset_lt_trans
∀[s:QOSet]. ∀[a,b,c:|s|].  (a <s c) supposing ((b <s c) and (a <s b))

Lemma: qoset_lt_irrefl
∀[s:QOSet]. ∀[a,b:|s|].  ¬(a = b ∈ |s|) supposing a <s b

Lemma: set_lt_irreflexivity
∀[s:QOSet]. ∀[a:|s|].  False supposing a <s a

Lemma: set_leq_weakening_lt
∀[s:QOSet]. ∀[a,b:|s|].  a ≤ b supposing a <s b

Lemma: set_lt_transitivity_1
∀[s:QOSet]. ∀[a,b,c:|s|].  (a <s c) supposing ((b <s c) and (a ≤ b))

Lemma: set_lt_transitivity_2
∀[s:QOSet]. ∀[a,b,c:|s|].  (a <s c) supposing ((b ≤ c) and (a <s b))

Lemma: set_blt_functionality_wrt_set_lt_r
∀[s:QOSet]. ∀[a,b,b':|s|].  ↑(a <b b ⇒b (a <b b')) supposing b <s b'

Definition: poset
POSet{i} ==  {s:QOSet| UniformlyAntiSym(|s|;a,b.a ≤ b)} 

Lemma: poset_wf
POSet{i} ∈ 𝕌'

Lemma: poset_subtype_qoset
POSet{i} ⊆r QOSet

Lemma: poset_properties
∀[s:POSet{i}]. UniformlyAntiSym(|s|;a,b.a ≤ b)

Lemma: poset_anti_sym
∀[s:POSet{i}]. ∀[a,b:|s|].  (a = b ∈ |s|) supposing ((b ≤ a) and (a ≤ b))

Lemma: set_leq_antisymmetry
∀[s:POSet{i}]. ∀[a,b:|s|].  (a = b ∈ |s|) supposing ((b ≤ a) and (a ≤ b))

Lemma: set_leq_iff_lt_or_eq
∀s:POSet{i}. ∀a,b:|s|.  (a ≤ b ⇐⇒ (a <s b) ∨ (a = b ∈ |s|))

Definition: loset
LOSet ==  {s:POSet{i}| Connex(|s|;x,y.x ≤ y)} 

Lemma: loset_wf
LOSet ∈ 𝕌'

Lemma: loset_subtype_poset
LOSet ⊆r POSet{i}

Lemma: loset_subtype_dset
LOSet ⊆r DSet

Lemma: loset_subtype_poset_sig
LOSet ⊆r PosetSig

Lemma: loset_properties
∀s:LOSet. Connex(|s|;x,y.x ≤ y)

Definition: mk_oset
mk_oset(T;eq;leq) ==  <T, eq, leq>

Lemma: mk_oset_wf
∀[T:Type]. ∀[eq,leq:T ⟶ T ⟶ 𝔹].
  (mk_oset(T;eq;leq) ∈ LOSet) supposing (UniformLinorder(T;a,b.↑(a leq b)) and IsEqFun(T;eq))

Lemma: loset_connex
∀s:LOSet. ∀x,y:|s|.  ((x ≤ y) ∨ (y ≤ x))

Lemma: loset_trichot
∀s:LOSet. ∀a,b:|s|.  ((a <s b) ∨ (a = b ∈ |s|) ∨ (b <s a))

Lemma: set_leq_complement
∀[s:LOSet]. ∀[a,b:|s|].  uiff(¬(a ≤ b);b <s a)

Lemma: set_lt_complement
∀[s:LOSet]. ∀[a,b:|s|].  uiff(¬(b <s a);a ≤ b)

Definition: eq_pair
a =b b ==  ((fst(a)) (=b) (fst(b))) ∧b ((snd(a)) (=b) (snd(b)))

Lemma: eq_pair_wf
∀[s,t:DSet]. ∀[a,b:|s| × |t|].  (a =b b ∈ 𝔹)

Lemma: assert_of_eq_pair
∀[s,t:DSet]. ∀[a,b:|s| × |t|].  uiff(↑(a =b b);a = b ∈ (|s| × |t|))

Definition: set_prod
s × t ==  mk_dset(|s| × |t|, λa,b. (a =b b))

Lemma: set_prod_wf
∀[s,t:DSet].  (s × t ∈ DSet)

Definition: dset_set
{x:s| Q[x]} ==  mk_dset({x:|s|| Q[x]} , =b)

Lemma: eqfun_p_subtyping
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[eq:T ⟶ T ⟶ 𝔹].  IsEqFun({x:T| P[x]} ;eq) supposing IsEqFun(T;eq)

Lemma: dset_set_wf
∀[s:DSet]. ∀[Q:|s| ⟶ ℙ].  ({x:s| Q[x]} ∈ DSet)

Definition: int_loset
int_loset() ==  mk_oset(ℤ;λx,y. (x =z y);λx,y. x ≤z y)

Lemma: int_loset_wf
int_loset() ∈ LOSet

Definition: atom_dset
atom_dset() ==  mk_dset(Atom, λx,y. x =a y)

Lemma: atom_dset_wf
atom_dset() ∈ DSet



Home Index