ordConnected_iff_upperClosure_inter_lowerClosure

English

A set s is OrdConnected if and only if ↑(upperClosure s) ∩ ↑(lowerClosure s) = s.

Русский

Множество s является OrdConnected тогда и только тогда, когда ↑(upperClosure s) ∩ ↑(lowerClosure s) = s.

LaTeX

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

Lean4

theorem ordConnected_iff_upperClosure_inter_lowerClosure : s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s :=
  by
  refine ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩
  rw [← h]
  exact (UpperSet.upper _).ordConnected.inter (LowerSet.lower _).ordConnected

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