Commit 2025-04-26 22:41 a7411a88

View on Github →

refactor(TangentCone): use AccPt (#24227)

  • weaken assumptions in zero_mem_tangentCone from (𝓝[s \ {x}] x).NeBot to x ∈ closure s;
  • change assumptions here and there from (𝓝[s \ {x}] x).NeBot to AccPt x (𝓟 s);
  • prove uniqueDiffWithinAt_iff_accPt.

Estimated changes

modified theorem tangentCone_eq_univ
modified theorem zero_mem_tangentCone