IsolatedZeros

📁 Source: Mathlib/Analysis/Meromorphic/IsolatedZeros.lean

Statistics

Metric	Count
Definitions	0
Theorems eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin, eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin, frequently_eq_iff_eventuallyEq, frequently_zero_iff_eventuallyEq_zero	4
Total	4

MeromorphicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin 📖	mathematical	MeromorphicAt Set Set.instMembership Filter.EventuallyEq Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet	—	Filter.eventuallyEq_iff_sub eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin sub
eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin 📖	mathematical	MeromorphicAt Set Set.instMembership Filter.EventuallyEq Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet	—	frequently_zero_iff_eventuallyEq_zero Filter.Frequently.mp Filter.Frequently.and_eventually accPt_iff_frequently_nhdsNE mem_codiscreteWithin_iff_forall_mem_nhdsNE Filter.univ_mem'
frequently_eq_iff_eventuallyEq 📖	mathematical	MeromorphicAt	Filter.Frequently nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet Filter.EventuallyEq	—	Filter.eventuallyEq_iff_sub frequently_zero_iff_eventuallyEq_zero sub
frequently_zero_iff_eventuallyEq_zero 📖	mathematical	MeromorphicAt	Filter.Frequently NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet Filter.EventuallyEq Pi.instZero	—	eventually_eq_zero_or_eventually_ne_zero Filter.Eventually.frequently PerfectSpace.not_isolated instPerfectSpace

---

← Back to Index