upperBounds_lowerClosure — Mathlib

English

Equivalent formulation of ordConnected: s.OrdConnected iff ↑(upperClosure s) ∩ ↑(lowerClosure s) = s.

Русский

Эквивалентная формулировка ordConnected: s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s.

LaTeX

$$s.OrdConnected \iff \uparrow(upperClosure s) \cap \uparrow(lowerClosure s) = s$$

Lean4

@[simp]
theorem upperBounds_lowerClosure : upperBounds (lowerClosure s : Set α) = upperBounds s :=
  (upperBounds_mono_set subset_lowerClosure).antisymm fun _a ha _b ⟨_c, hc, hcb⟩ ↦ hcb.trans <| ha hc

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