mem_map_equiv — Mathlib

English

For a ring equivalence f : R ≃+* S and K a nonunital subsemiring of R, x ∈ K.map f iff f^{-1}(x) ∈ K.

Русский

Для равносильного отображения f : R ≃+* S и K ⊆ R, x ∈ K.map f эквивалентно f^{-1}(x) ∈ K.

LaTeX

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

Lean4

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

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