dual — Mathlib

English

If s is an OrdConnected subset, then its dual preimage under the dual order is OrdConnected.

Русский

Если s —OrdConnected множество, то его дуальная предобразная под порядок дуального типа также OrdConnected.

LaTeX

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

Lean4

theorem dual {s : Set α} (hs : OrdConnected s) : OrdConnected (OrderDual.ofDual ⁻¹' s) :=
  ⟨fun _ hx _ hy _ hz => hs.out hy hx ⟨hz.2, hz.1⟩⟩

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