preimage — Mathlib

English

Let s be sup-closed in α and f: F → α be a sup-homomorphism. Then the preimage f⁻¹(s) is sup-closed in β.

Русский

Пусть s замкнуто по ⊔ в α и f: F → α — гомоморфизм по ⊔. Тогда предобраз f⁻¹(s) в β тоже замкнут по ⊔.

LaTeX

$$$ (\\forall x \\in f^{-1}(s))(\\forall y \\in f^{-1}(s))\\, (x \\sqcup y) \\in f^{-1}(s)$$$

Lean4

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

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