---

Step * 1 1 1 1 of Lemma cut-of-singleton


1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c')
8. {e} ⊆ cut(X;f;{e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c')
9. ↑e ∈b prior(X)
10. (f e) = e ∈ E
11. {prior(X)(e)} ⊆ cut(X;f;{prior(X)(e)}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{prior(X)(e)}) ⊆ c' supposing {prior(X)(e)} ⊆ c')
⊢ cut(X;f;{e}) = {e} ∪ cut(X;f;{prior(X)(e)}) ∈ fset(E(X))
BY
{ (Using [`eq',⌈es-eq(es)⌉] (BLemma `f-subset_antisymmetry`)⋅ THEN Auto)⋅ }

1
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e})
8. ∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c'
9. {e} ⊆ cut(X;f;{e})
10. ∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c'
11. ↑e ∈b prior(X)
12. (f e) = e ∈ E
13. {prior(X)(e)} ⊆ cut(X;f;{prior(X)(e)})
14. ∀[c':Cut(X;f)]. cut(X;f;{prior(X)(e)}) ⊆ c' supposing {prior(X)(e)} ⊆ c'
⊢ cut(X;f;{e}) ⊆ {e} ∪ cut(X;f;{prior(X)(e)})

2
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e})
8. ∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c'
9. {e} ⊆ cut(X;f;{e})
10. ∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c'
11. ↑e ∈b prior(X)
12. (f e) = e ∈ E
13. {prior(X)(e)} ⊆ cut(X;f;{prior(X)(e)})
14. ∀[c':Cut(X;f)]. cut(X;f;{prior(X)(e)}) ⊆ c' supposing {prior(X)(e)} ⊆ c'
⊢ {e} ∪ cut(X;f;{prior(X)(e)}) ⊆ cut(X;f;{e})

---

Latex:

---

Latex:

1.  Info  :  Type@i'
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  f  :  sys-antecedent(es;X)@i
5.  e  :  E(X)@i
6.  \mforall{}[s:fset(E(X))].  (s  \msubseteq{}  cut(X;f;s)  \mwedge{}  (\mforall{}[c':Cut(X;f)].  cut(X;f;s)  \msubseteq{}  c'  supposing  s  \msubseteq{}  c'))
7.  \{f  e\}  \msubseteq{}  cut(X;f;\{f  e\})  \mwedge{}  (\mforall{}[c':Cut(X;f)].  cut(X;f;\{f  e\})  \msubseteq{}  c'  supposing  \{f  e\}  \msubseteq{}  c')
8.  \{e\}  \msubseteq{}  cut(X;f;\{e\})  \mwedge{}  (\mforall{}[c':Cut(X;f)].  cut(X;f;\{e\})  \msubseteq{}  c'  supposing  \{e\}  \msubseteq{}  c')
9.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
10.  (f  e)  =  e
11.  \{prior(X)(e)\}  \msubseteq{}  cut(X;f;\{prior(X)(e)\})
\mwedge{}  (\mforall{}[c':Cut(X;f)].  cut(X;f;\{prior(X)(e)\})  \msubseteq{}  c'  supposing  \{prior(X)(e)\}  \msubseteq{}  c')
\mvdash{}  cut(X;f;\{e\})  =  \{e\}  \mcup{}  cut(X;f;\{prior(X)(e)\})


By

---

Latex:
(Using  [`eq',\mkleeneopen{}es-eq(es)\mkleeneclose{}]  (BLemma  `f-subset\_antisymmetry`)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index