---

Step * of 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))
BY
{ Unfold `mk_oset` 0 
THEN ((RepD) THENA Auto) }

1
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. leq : T ⟶ T ⟶ 𝔹
4. IsEqFun(T;eq)
5. UniformLinorder(T;a,b.↑(a leq b))
⊢ <T, eq, leq> ∈ LOSet

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq,leq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
    (mk\_oset(T;eq;leq)  \mmember{}  LOSet)  supposing  (UniformLinorder(T;a,b.\muparrow{}(a  leq  b))  and  IsEqFun(T;eq))


By

---

Latex:
Unfold  `mk\_oset`  0 
THEN  ((RepD)  THENA  Auto)

---

Home Index