preimage_anti — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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