span_eq_top_of_surjective — Mathlib

English

If f is surjective and the span of s is top, then the span of the image is top.

Русский

Если отображение сюръективно и афинное замыкание множества равно верхнему, то афинное замыкание его изображения также равно верхнему.

LaTeX

$$$ hf:\\ Function.Surjective\\ f \\land h: affineSpan k s = \\top \\Rightarrow affineSpan k (f '' s) = \\top$$$

Lean4

theorem span_eq_top_of_surjective {s : Set P₁} (hf : Function.Surjective f) (h : affineSpan k s = ⊤) :
    affineSpan k (f '' s) = ⊤ := by rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]

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