dual_ordConnected_iff — Mathlib

English

The OrdConnected property is preserved under taking the order dual: OrdConnected(ofDual^{-1}(s)) is equivalent to OrdConnected(s).

Русский

Свойство упорядоченно связного сохраняется при переходе к двойственному порядку: OrdConnected(ofDual^{-1}(s)) эквивалентно OrdConnected(s).

LaTeX

$$$\\operatorname{OrdConnected}(\\mathrm{ofDual}^{-1}(s)) \\iff \\operatorname{OrdConnected}(s)$$$

Lean4

@[simp]
theorem dual_ordConnected_iff {s : Set α} : OrdConnected (ofDual ⁻¹' s) ↔ OrdConnected s :=
  by
  simp_rw [ordConnected_def, toDual.surjective.forall, Icc_toDual, Subtype.forall']
  exact forall_swap

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