preimage_coe_affineSpan_singleton

English

The preimage of the singleton {x} under the inclusion from affineSpan k({x}) to P is the whole domain affineSpan k({x}).

Русский

Обратное изображение множества {x} при включении affineSpan_k({x}) в P равно всему домену affineSpan_k({x}).

LaTeX

$$$ (\\uparrow)^{-1}(\\\\{x\\\\}) = univ $$$

Lean4

@[simp]
theorem preimage_coe_affineSpan_singleton (x : P) : ((↑) : affineSpan k ({ x } : Set P) → P) ⁻¹' { x } = univ :=
  eq_univ_of_forall fun y => (AffineSubspace.mem_affineSpan_singleton _ _).1 y.2

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