preimage — Mathlib

English

If s is inf-closed and f is an inf-preserving map, then the preimage f⁻¹'(s) is inf-closed.

Русский

Если s инф-замкнуто и f сохраняет infimum, то предобраз f⁻¹'(s) инф-замкнут.

LaTeX

$$$ [\\text{InfHomClass } F \\ β α] \\rightarrow (\\text{InfClosed } s) \\rightarrow \\text{InfClosed}(f^{-1}(s)) $$$

Lean4

theorem preimage [FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) : InfClosed (f ⁻¹' s) := fun a ha b hb ↦
  by simpa [map_inf] using hs ha hb

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