nonempty_map — Mathlib

English

If E is nonempty, then its image under an affine map φ is nonempty.

Русский

Если E непусто, то образ E под аффинным отображением φ непуст.

LaTeX

$$$ E \\neq \\varnothing \\Rightarrow E.map \\phi \\neq \\varnothing $$$

Lean4

instance nonempty_map {E : AffineSubspace k P₁} [Ene : Nonempty E] {φ : P₁ →ᵃ[k] P₂} : Nonempty (E.map φ) :=
  by
  obtain ⟨x, hx⟩ := id Ene
  exact ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩

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