oangle_sign_smul_add_right — Mathlib

English

Let V be a 2-dimensional real inner product space with orientation o. For any x,y in V and any real r, the sign of o.oangle(x, r·x + y) equals the sign of o.oangle(x, y).

Русский

Пусть V — двумерное вещественное пространство с ориентировкой o. Для любых x,y ∈ V и любого r ∈ ℝ знак o.oangle(x, r·x + y) равен знаку o.oangle(x,y).

LaTeX

$$$\\forall x,y\\in V,\\ r\\in\\mathbb{R},\\ \\operatorname{sign}\\big(o.oangle(x, r\\,x+y)\\big) = \\operatorname{sign}\\big(o.oangle(x,y)\\big)$$$

Lean4

/-- Adding a multiple of the first vector passed to `oangle` to the second vector does not change
the sign of the angle. -/
@[simp]
theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) : (o.oangle x (r • x + y)).sign = (o.oangle x y).sign :=
  by
  by_cases h : o.oangle x y = 0 ∨ o.oangle x y = π
  · rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff, oangle_smul_add_right_eq_zero_or_eq_pi_iff]
  have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π :=
    by
    intro r'
    rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h
  let s : Set (V × V) := (fun r' : ℝ => (x, r' • x + y)) '' Set.univ
  have hc : IsConnected s := isConnected_univ.image _ (by fun_prop)
  have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s :=
    by
    refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_
    all_goals
      simp_rw [s, Set.mem_image] at hz
      obtain ⟨r', -, rfl⟩ := hz
      simp only
      intro hz
    · simpa [hz] using (h' 0).1
    · simpa [hz] using (h' r').1
  have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := by grind
  have hx : (x, y) ∈ s :=
    by
    convert Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0)
    simp
  have hy : (x, r • x + y) ∈ s := Set.mem_image_of_mem _ (Set.mem_univ _)
  convert Real.Angle.sign_eq_of_continuousOn hc hf hs hx hy

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