mem_map_equiv — Mathlib

English

Let f be a semiring isomorphism between R and S. For any Subsemiring K of R and any x ∈ S, x ∈ K.map f iff f^{-1}(x) ∈ K.

Русский

Пусть f — изоморфизм полусемиринга между R и S. Тогда для любого подsemiring K ⊆ R и любого x ∈ S выполняется x ∈ K.map f ⇔ f^{-1}(x) ∈ K.

LaTeX

$$$x \\in K.map (f : R \\to R) \\iff f^{-1}(x) \\in K$$$

Lean4

theorem mem_map_equiv {f : R ≃+* S} {K : Subsemiring R} {x : S} : x ∈ K.map (f : R →+* S) ↔ f.symm x ∈ K := by
  convert @Set.mem_image_equiv _ _ (↑K) f.toEquiv x using 1

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