preimage_mono — Mathlib

English

If s is OrdConnected and f is monotone, then the preimage f^{-1}(s) is OrdConnected.

Русский

Если s OrdConnected и f монотонна, то preimage f^{-1}(s) также OrdConnected.

LaTeX

$$$\operatorname{OrdConnected}(s) \wedge \operatorname{Monotone}(f) \Rightarrow \operatorname{OrdConnected}(f^{-1}(s)).$$$

Lean4

theorem preimage_mono {f : β → α} (hs : OrdConnected s) (hf : Monotone f) : OrdConnected (f ⁻¹' s) :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨hf hz.1, hf hz.2⟩⟩

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