---

Step * 2 of Lemma omon_properties


1. g : AbMon
2. UniformLinorder(|g|;x,y.↑(x ≤b y))
3. =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)
4. UniformLinorder(|g|;x,y.↑(x ≤b y))
⊢ IsEqFun(|g|;=b)
BY
{ ((HypSubst (-2) 0 THEN Auto) THEN D 0 THEN Reduce 0 THEN Auto) }

1
1. g : AbMon
2. UniformLinorder(|g|;x,y.↑(x ≤b y))
3. =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)
4. UniformLinorder(|g|;x,y.↑(x ≤b y))
5. x : |g|
6. y : |g|
7. ↑((x ≤b y) ∧b (y ≤b x))
⊢ x = y ∈ |g|

---

Latex:

---

Latex:

1.  g  :  AbMon
2.  UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
3.  =\msubb{}  =  (\mlambda{}x,y.  ((x  \mleq{}\msubb{}  y)  \mwedge{}\msubb{}  (y  \mleq{}\msubb{}  x)))
4.  UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
\mvdash{}  IsEqFun(|g|;=\msubb{})


By

---

Latex:
((HypSubst  (-2)  0  THEN  Auto)  THEN  D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index