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