Theorem one_mem_posTangentConeAt_iff_mem_closure

Modification history

2024-07-13 21:21

Mathlib/Analysis/Calculus/LocalExtr/Basic.lean

feat(LocalExtr/Basic): add lemmas about `_ ∈ posTangentConeAt _ _` (#14434)

Added one_mem_posTangentConeAt_iff_mem_closure View on Github →