map_mem_map — Mathlib

English

If f is injective, then membership is preserved along map: f x ∈ map f I iff x ∈ I.

Русский

Если f инъективно, то принадлежность сохраняется при отображении: f x ∈ map f I эквивалентно x ∈ I.

LaTeX

$$$ f x \\in \\mathrm{map} f I \\ \\iff\\ \\ x \\in I $$$

Lean4

theorem map_mem_map {f : P →ₐ[R] P'} (h : Function.Injective f) {x : P} {I : FractionalIdeal S P} :
    f x ∈ map f I ↔ x ∈ I :=
  mem_map.trans ⟨fun ⟨_, hx', x'_eq⟩ => h x'_eq ▸ hx', fun h => ⟨x, h, rfl⟩⟩

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