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	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set 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	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	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