Oscillation

📁 Source: Mathlib/Analysis/Oscillation.lean

Statistics

Metric	Count
Definitions oscillation, oscillationWithin	2
Theorems oscillation_eq_zero, oscillationWithin_eq_zero, uniform_oscillation, uniform_oscillationWithin, eq_zero_iff_continuousAt, eq_zero_iff_continuousWithinAt, oscillationWithin_nhds_eq_oscillation, oscillationWithin_univ_eq_oscillation	8
Total	10

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oscillation_eq_zero 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	oscillation ENNReal instZeroENNReal	—	ContinuousWithinAt.oscillationWithin_eq_zero continuousWithinAt_univ oscillationWithin_univ_eq_oscillation

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oscillationWithin_eq_zero 📖	mathematical	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	oscillationWithin ENNReal instZeroENNReal	—	le_antisymm le_of_forall_pos_le_add ENNReal.instDenselyOrdered CanonicallyOrderedAdd.toExistsAddOfLE ENNReal.instCanonicallyOrderedAdd ENNReal.addLeftReflectLT zero_add Nat.instAtLeastTwoHAddOfNat Metric.eball_mem_nhds ne_of_gt LE.le.trans biInf_le Metric.ediam_eball_le ENNReal.mul_div_cancel ENNReal.instCharZero zero_le

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniform_oscillation 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder oscillation	Real Real.instLT Real.instZero Preorder.toLE Metric.ediam Set.image Metric.eball ENNReal.ofReal	—	Set.inter_univ uniform_oscillationWithin
uniform_oscillationWithin 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder oscillationWithin	Real Real.instLT Real.instZero Preorder.toLE Metric.ediam Set.image Set Set.instInter Metric.eball ENNReal.ofReal	—	EMetric.isOpen_iff Nat.instAtLeastTwoHAddOfNat PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instIsOrderedRing Real.instNontrivial lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true le_trans Metric.ediam_mono Set.image_mono lt_of_le_of_lt PseudoEMetricSpace.edist_triangle ENNReal.add_lt_add ENNReal.ofReal_add le_of_not_gt Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg sub_add_cancel iInf_congr_Prop EMetric.mem_nhdsWithin_iff Set.iUnion_congr_Prop le_imp_le_of_le_of_le le_refl le_of_lt Set.image_subset_iff Set.inter_subset_inter Metric.eball_subset_eball subset_refl Set.instReflSubset one_pos Real.instZeroLEOneClass NeZero.charZero_one exists_between LinearOrderedSemiField.toDenselyOrdered ENNReal.toReal_pos ne_of_gt ENNReal.ofReal_toReal_le elim_finite_subcover_image Set.Finite.isWF Set.IsWF.min_mem Set.mem_iUnion Set.IsWF.min_le subset_trans Set.instIsTransSubset Set.not_nonempty_iff_eq_empty Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty ENNReal.ofReal_le_ofReal

Oscillation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_iff_continuousAt 📖	mathematical	—	oscillation ENNReal instZeroENNReal ContinuousAt UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	oscillationWithin_univ_eq_oscillation continuousWithinAt_univ OscillationWithin.eq_zero_iff_continuousWithinAt Set.mem_univ

OscillationWithin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_iff_continuousWithinAt 📖	mathematical	Set Set.instMembership	oscillationWithin ENNReal instZeroENNReal ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	EMetric.tendsto_nhds Filter.mem_of_superset lt_of_le_of_lt Metric.edist_le_ediam_of_mem Set.mem_preimage mem_of_mem_nhdsWithin ContinuousWithinAt.oscillationWithin_eq_zero

(root)

Definitions

Name	Category	Theorems
oscillation 📖	CompOp	4 math math: Oscillation.eq_zero_iff_continuousAt, oscillationWithin_nhds_eq_oscillation, oscillationWithin_univ_eq_oscillation, ContinuousAt.oscillation_eq_zero
oscillationWithin 📖	CompOp	4 math math: ContinuousWithinAt.oscillationWithin_eq_zero, oscillationWithin_nhds_eq_oscillation, oscillationWithin_univ_eq_oscillation, OscillationWithin.eq_zero_iff_continuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oscillationWithin_nhds_eq_oscillation 📖	mathematical	Set Filter Filter.instMembership nhds	oscillationWithin oscillation	—	oscillation.eq_1 oscillationWithin.eq_1 nhdsWithin_eq_nhds
oscillationWithin_univ_eq_oscillation 📖	mathematical	—	oscillationWithin Set.univ oscillation	—	oscillationWithin_nhds_eq_oscillation Filter.univ_mem

---

← Back to Index