ordConnected_dual — Mathlib

English

OrdConnected of a set and its dual preimage are equivalent: OrdConnected(s) iff OrdConnected( OrderDual.ofDual ⁻¹' s ).

Русский

OrdConnected множества эквивалентно OrdConnected его дуальной предобразной: OrdConnected(s) ⇔ OrdConnected( OrderDual.ofDual ⁻¹' s ).

LaTeX

$$$\operatorname{OrdConnected}( (OrderDual.ofDual)^{-1}' s ) \iff \operatorname{OrdConnected}(s)$$$

Lean4

theorem ordConnected_dual {s : Set α} : OrdConnected (OrderDual.ofDual ⁻¹' s) ↔ OrdConnected s :=
  ⟨fun h => by simpa only [ordConnected_def] using h.dual, fun h => h.dual⟩

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