ordConnected_preimage — Mathlib

English

If f is an order-preserving map, and s is OrdConnected in β, then the preimage f^{-1}(s) is OrdConnected in α.

Русский

Если f~ упорядочивающее отображение и s OrdConnected в β, то предобраз f^{-1}(s) в α также OrdConnected.

LaTeX

$$$\text{(f is an order-preserving map)}\; \Rightarrow\; \operatorname{OrdConnected}(f^{-1}(s))$$

Lean4

@[instance]
theorem ordConnected_preimage {F : Type*} [FunLike F α β] [OrderHomClass F α β] (f : F) {s : Set β}
    [hs : OrdConnected s] : OrdConnected (f ⁻¹' s) :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨OrderHomClass.mono _ hz.1, OrderHomClass.mono _ hz.2⟩⟩

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