English
A point lies on the perpendicular bisector of p1p2 iff the inner product with the segment direction is zero at the midpoint.
Русский
Точка принадлежит перпендикулярной биссектрисе отрезка p1p2 тогда и только тогда, когда скалярное произведение вектора p2−p1 с вектором x−середина равно нулю в смысле среднего.
LaTeX
$$$c \in \operatorname{perpBisector}(p_1,p_2) \iff \langle p_2-p_1, c-\text{midpoint}(p_1,p_2)\rangle = 0$$$
Lean4
/-- Suppose we are given a triangle `t₁`, and replace one of its
vertices by its orthocenter, yielding triangle `t₂` (with vertices not
necessarily listed in the same order). Then an altitude of `t₂` from
a vertex that was not replaced is the corresponding side of `t₁`. -/
theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3} (hi₁₂ : i₁ ≠ i₂)
(hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₂₃ : j₂ ≠ j₃)
(h₁ : t₂.points j₁ = t₁.orthocenter) (h₂ : t₂.points j₂ = t₁.points i₂) (h₃ : t₂.points j₃ = t₁.points i₃) :
t₂.altitude j₂ = line[ℝ, t₁.points i₁, t₁.points i₂] :=
by
symm
rw [← h₂, t₂.affineSpan_pair_eq_altitude_iff]
rw [h₂]
use t₁.independent.injective.ne hi₁₂
have he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points) :=
by
refine ext_of_direction_eq ?_ ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (Set.mem_range_self _)⟩
refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_le_of_subset_coe ?_)) ?_
· have hu : (Set.univ : Set (Fin 3)) = { j₁, j₂, j₃ } :=
by
clear h₁ h₂ h₃
ext
decide +revert
rw [← Set.image_univ, hu, Set.image_insert_eq, Set.image_insert_eq, Set.image_singleton, h₁, h₂, h₃,
Set.insert_subset_iff, Set.insert_subset_iff, Set.singleton_subset_iff]
exact
⟨t₁.orthocenter_mem_affineSpan, mem_affineSpan ℝ (Set.mem_range_self _),
mem_affineSpan ℝ (Set.mem_range_self _)⟩
·
rw [direction_affineSpan, direction_affineSpan, t₁.independent.finrank_vectorSpan (Fintype.card_fin _),
t₂.independent.finrank_vectorSpan (Fintype.card_fin _)]
rw [he]
use mem_affineSpan ℝ (Set.mem_range_self _)
have hu : ({ j₂ }ᶜ : Set _) = { j₁, j₃ } := by
clear h₁ h₂ h₃
ext
decide +revert
rw [hu, Set.image_insert_eq, Set.image_singleton, h₁, h₃]
have hle : (t₁.altitude i₃).directionᗮ ≤ line[ℝ, t₁.orthocenter, t₁.points i₃].directionᗮ :=
Submodule.orthogonal_le (direction_le (affineSpan_orthocenter_point_le_altitude _ _))
refine hle ((t₁.vectorSpan_isOrtho_altitude_direction i₃) ?_)
have hui : ({ i₃ }ᶜ : Set _) = { i₁, i₂ } := by
clear hle h₂ h₃
ext
decide +revert
rw [hui, Set.image_insert_eq, Set.image_singleton]
exact vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))
