Within

📁 Source: Mathlib/Analysis/Analytic/Within.lean

Statistics

Metric	Count
Definitions	0
Theorems eventually_analyticWithinAt, exists_analyticAt, exists_mem_nhdsWithin_analyticOn, analyticOn_iff_analyticOnNhd, analyticOn_of_locally_analyticOn, analyticWithinAt_iff_exists_analyticAt, analyticWithinAt_iff_exists_analyticAt', analyticWithinAt_of_singleton_mem, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt, hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall	10
Total	10

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_analyticWithinAt 📖	mathematical	AnalyticWithinAt	Filter.Eventually nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	analyticWithinAt_iff_exists_analyticAt Filter.mp_mem AnalyticAt.eventually_analyticAt Filter.Eventually.eventually_nhds Filter.univ_mem' Filter.Eventually.filter_mono nhdsWithin_mono Set.insert_eq_of_mem eventually_nhdsWithin_iff
exists_analyticAt 📖	mathematical	AnalyticWithinAt	Set.EqOn Set Set.instInsert AnalyticAt	—	analyticWithinAt_iff_exists_analyticAt'
exists_mem_nhdsWithin_analyticOn 📖	mathematical	AnalyticWithinAt	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert AnalyticOn	—	exists_analyticAt inter_mem_nhdsWithin IsOpen.mem_nhds isOpen_analyticAt AnalyticAt.analyticWithinAt congr Set.EqOn.mono Set.inter_subset_left

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn_iff_analyticOnNhd 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AnalyticOn AnalyticOnNhd	—	Metric.mem_nhds_iff mem_nhds min_le_of_right_le HasFPowerSeriesWithinOnBall.r_le lt_min ENNReal.ofReal_pos HasFPowerSeriesWithinOnBall.r_pos HasFPowerSeriesWithinOnBall.hasSum Set.mem_insert_of_mem dist_self_add_left dist_zero_right AnalyticOnNhd.analyticOn

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn_of_locally_analyticOn 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership AnalyticOn Set.instInter	—	—	Metric.mem_nhds_iff IsOpen.mem_nhds min_le_of_right_le HasFPowerSeriesWithinOnBall.r_le lt_min ENNReal.ofReal_pos HasFPowerSeriesWithinOnBall.r_pos HasFPowerSeriesWithinOnBall.hasSum AddLeftCancelSemigroup.toIsLeftCancelAdd add_zero dist_zero_right dist_self_add_left
analyticWithinAt_iff_exists_analyticAt 📖	mathematical	—	AnalyticWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert AnalyticAt	—	—
analyticWithinAt_iff_exists_analyticAt' 📖	mathematical	—	AnalyticWithinAt Set.EqOn Set Set.instInsert AnalyticAt	—	mem_nhdsWithin Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem AnalyticAt.congr Filter.mp_mem IsOpen.mem_nhds Filter.univ_mem' self_mem_nhdsWithin
analyticWithinAt_of_singleton_mem 📖	mathematical	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instSingletonSet	AnalyticWithinAt	—	mem_nhdsWithin Metric.mem_nhds_iff IsOpen.mem_nhds UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup FormalMultilinearSeries.constFormalMultilinearSeries_radius ENNReal.ofReal_pos AddLeftCancelSemigroup.toIsLeftCancelAdd add_zero dist_self_add_left Metric.eball_ofReal dist_zero_right HasFPowerSeriesOnBall.hasSum hasFPowerSeriesOnBall_const Metric.eball_top
hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt 📖	mathematical	—	HasFPowerSeriesWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert HasFPowerSeriesAt	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall Filter.eventuallyEq_iff_exists_mem inter_mem_nhdsWithin Metric.eball_mem_nhds HasFPowerSeriesOnBall.r_pos HasFPowerSeriesOnBall.mono lt_min ENNReal.ofReal_pos min_le_left
hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall 📖	mathematical	—	HasFPowerSeriesWithinOnBall Set.EqOn Set Set.instInter Set.instInsert Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace HasFPowerSeriesOnBall	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.hasSum edist_zero_right lt_of_lt_of_le edist_eq_enorm_sub HasFPowerSeriesWithinOnBall.r_le HasFPowerSeriesWithinOnBall.hasSum add_sub_cancel HasSum.unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional HasFPowerSeriesWithinOnBall.r_pos add_sub_cancel_left HasFPowerSeriesOnBall.r_le HasFPowerSeriesOnBall.r_pos sub_zero HasFPowerSeriesOnBall.hasSum

---

← Back to Index