upperClosure_inter_lowerClosure — Mathlib

English

If s is OrdConnected, then the intersection of the images under upperClosure and lowerClosure equals s: ↑(upperClosure s) ∩ ↑(lowerClosure s) = s.

Русский

Если s является ord-connected, то пересечение образов верхнего и нижнего замыкания равно s.

LaTeX

$$↑(upperClosure s) ∩ ↑(lowerClosure s) = s \quad\text{for } s.OrdConnected$$

Lean4

theorem upperClosure_inter_lowerClosure (h : s.OrdConnected) : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s :=
  (subset_inter subset_upperClosure subset_lowerClosure).antisymm' fun _a ⟨⟨_b, hb, hba⟩, _c, hc, hac⟩ =>
    h.out hb hc ⟨hba, hac⟩

Похожие утверждения