English
Let s be an orthocentric system of points in P. For any injective triple p: Fin 3 → P with range contained in s, the affine span of the three points agrees with the affine span of s.
Русский
Пусть s — ортокцентрическая система точек в пространстве P. Для любых инъективных трёх точек p: Fin 3 → P, лежащих в s, аффинная оболочка трёх точек совпадает с аффинной оболочкой всей системы s.
LaTeX
$$$\\operatorname{affineSpan}_{\\mathbb{R}}(\\mathrm{range}(p)) = \\operatorname{affineSpan}_{\\mathbb{R}}(s)\\,.$$$
Lean4
/-- Any three points in an orthocentric system span the same subspace
as the whole orthocentric system. -/
theorem affineSpan_of_orthocentricSystem {s : Set P} (ho : OrthocentricSystem s) {p : Fin 3 → P} (hps : Set.range p ⊆ s)
(hpi : Function.Injective p) : affineSpan ℝ (Set.range p) = affineSpan ℝ s :=
by
have ha := ho.affineIndependent hps hpi
rcases ho with ⟨t, _, hts⟩
have hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points) := by
rw [hts, affineSpan_insert_eq_affineSpan ℝ t.orthocenter_mem_affineSpan]
refine
ext_of_direction_eq ?_ ⟨p 0, mem_affineSpan ℝ (Set.mem_range_self _), mem_affineSpan ℝ (hps (Set.mem_range_self _))⟩
have hfd : FiniteDimensional ℝ (affineSpan ℝ s).direction := by rw [hs]; infer_instance
refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_mono ℝ hps)) ?_
rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _),
t.independent.finrank_vectorSpan (Fintype.card_fin _)]
