sign_signedInfDist_lineMap_excenter_touchpoint

English

Along the line from the incenter through a touchpoint, the sign of the signed distance remains constant for r in [0,1].

Русский

Аналогично случаю с эксцентрическим, но для инцентра; знак сохраняется при линейном отображении через точку касания.

LaTeX

$$$ SignType.sign\left( s.signedInfDist_j\left(\mathrm{AffineMap.lineMap}(s.incenter, s.touchpoint(i), r)\right)\right) = SignType.sign\left( s.signedInfDist_j( s.incenter ) \right) \quad (r \in [0,1]) $$$

Lean4

theorem sign_signedInfDist_lineMap_excenter_touchpoint {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs)
    {i j : Fin (n + 1)} (hne : i ≠ j) {r : ℝ} (hr : r ∈ Set.Icc 0 1) :
    SignType.sign (s.signedInfDist j (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) r)) =
      SignType.sign (s.signedInfDist j (s.excenter signs)) :=
  by
  have hc :
    ContinuousOn
      (fun (t : ℝ) ↦ SignType.sign (s.signedInfDist j (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) t)))
      (Set.Icc 0 1) :=
    by
    refine
      continuousOn_of_forall_continuousAt fun t ht ↦
        ((continuousAt_sign_of_ne_zero ?_).comp (((s.signedInfDist j).cont.comp ?_).continuousAt))
    · intro h0
      rw [← abs_eq_zero, abs_signedInfDist_eq_dist_of_mem_affineSpan_range] at h0
      · rw [orthogonalProjectionSpan, dist_orthogonalProjection_eq_zero_iff] at h0
        by_cases ht1 : t = 1
        · subst ht1
          rw [AffineMap.lineMap_apply_one] at h0
          exact h.touchpoint_notMem_affineSpan_of_ne hne h0
        · refine (h.isTangentAt_touchpoint j).isTangent.notMem_of_dist_lt ?_ h0
          simp only [exsphere_center, dist_lineMap_left, Real.norm_eq_abs, h.dist_excenter, exsphere_radius,
            h.exradius_pos, mul_lt_iff_lt_one_left]
          rw [abs_lt]
          rcases ht with ⟨ht0, ht1'⟩
          exact ⟨by linarith, ht1'.lt_of_ne ht1⟩
      · exact AffineMap.lineMap_mem _ h.excenter_mem_affineSpan_range (s.touchpoint_mem_affineSpan_simplex _ _)
    · rw [← ContinuousAffineMap.lineMap_toAffineMap]
      exact ContinuousAffineMap.cont _
  refine ((isConnected_Icc zero_le_one).image _ hc).isPreconnected.subsingleton (Set.mem_image_of_mem _ hr) ?_
  convert Set.mem_image_of_mem _ (Set.left_mem_Icc.2 (zero_le_one' ℝ))
  simp

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