map_bot — Mathlib

English

The image of a subspace under an affine map is bottom if and only if the subspace is bottom.

Русский

Образ подпространства при аффинном отображении равен нижнему тогда и только тогда, когда подпространство равно нижнему.

LaTeX

$$$s.map f = \\perp \\iff s = \\perp$$$

Lean4

@[simp]
theorem map_bot : (⊥ : AffineSubspace k P₁).map f = ⊥ :=
  coe_injective <| image_empty f

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