dual_ordConnected — Mathlib

English

If s is OrdConnected, then its preimage under OrderDual.ofDual is OrdConnected.

Русский

Если s упорядоченно связно, то прообраз под OrderDual.ofDual также упорядоченно связан.

LaTeX

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

Lean4

@[instance]
theorem dual_ordConnected {s : Set α} [OrdConnected s] : OrdConnected (ofDual ⁻¹' s) :=
  dual_ordConnected_iff.2 ‹_›

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