mem_and_mem_iff_eq — Mathlib

English

If s.IsTangentAt p to as, then q ∈ s and q ∈ as iff q = p.

Русский

Если s касается p к as, то для точки q: q ∈ s и q ∈ as тогда и только тогда, когда q = p.

LaTeX

$$$ (q \\in s) \\land (q \\in as) \\iff q = p $$$

Lean4

theorem mem_and_mem_iff_eq {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) :
    (q ∈ s ∧ q ∈ as) ↔ q = p := by
  refine ⟨fun ⟨hs, has⟩ ↦ ?_, ?_⟩
  · have hd := h.dist_sq_eq_of_mem has
    rw [hs] at hd
    simpa using hd
  · rintro rfl
    exact ⟨h.mem_sphere, h.mem_space⟩

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