mem_map_iff_mem_of_injective — Mathlib

English

The image of the bottom subspace under any affine map is the bottom subspace.

Русский

Образ нулевого (нижнего) подпространства под любым аффинным отображением равен нулевому.

LaTeX

$$$\\big(\\perp : \\text{AffineSubspace}_k P_1\\big).map f = \\perp$$$

Lean4

@[simp 1100]
theorem mem_map_iff_mem_of_injective {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₁} (hf : Function.Injective f) :
    f x ∈ s.map f ↔ x ∈ s :=
  hf.mem_set_image

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