English
The vertex and the foot of the altitude are distinct points.
Русский
Вершина и опорная точка высоты различны.
LaTeX
$$$s.\mathrm{points}(i) \neq s.\mathrm{altitudeFoot}(i)$$$
Lean4
/-- A line through a vertex is the altitude through that vertex if and
only if it is orthogonal to the opposite face. -/
theorem affineSpan_pair_eq_altitude_iff {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) (p : P) :
line[ℝ, p, s.points i] = s.altitude i ↔
p ≠ s.points i ∧
p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' { i }ᶜ)).directionᗮ :=
by
rw [eq_iff_direction_eq_of_mem (mem_affineSpan ℝ (Set.mem_insert_of_mem _ (Set.mem_singleton _))) (s.mem_altitude _),
← vsub_right_mem_direction_iff_mem (mem_affineSpan ℝ (Set.mem_range_self i)) p, direction_affineSpan,
direction_affineSpan, direction_affineSpan]
constructor
· intro h
constructor
· intro heq
rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h
have hd : finrank ℝ (s.altitude i).direction = 0 := by rw [← h, finrank_bot]
simp at hd
· rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude, ← h]
exact vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))
· rintro ⟨hne, h⟩
rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude] at h
rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _), Set.insert_diff_of_mem _ (Set.mem_singleton _),
Set.diff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton]
refine Submodule.eq_of_le_of_finrank_eq ?_ ?_
· rw [Submodule.span_le]
simpa using h
· rw [finrank_direction_altitude, finrank_span_set_eq_card]
· simp
· exact LinearIndepOn.id_singleton _ <| by simpa using hne
