Lemmas

📁 Source: Mathlib/Topology/Instances/Real/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems compact_of_continuous, isBounded_of_continuous, cobounded_eq, continuous_inv, exists_seq_rat_strictAnti_tendsto, exists_seq_rat_strictMono_tendsto, isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici, isGLB_of_tendsto_antitone_bddBelow, isLUB_of_tendsto_monotoneOn_bddAbove_nat_Ici, isLUB_of_tendsto_monotone_bddAbove, isTopologicalBasis_Ioo_rat, mem_closure_iff, subfield_eq_of_closed, tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici, tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici, totallyBounded_ball, uniformContinuous_abs, uniformContinuous_inv, uniformContinuous_mul, closure_of_rat_image_lt, closure_ordConnected_inter_rat	21
Total	21

Function.Periodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compact_of_continuous 📖	mathematical	Function.Periodic Real Real.instAdd Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	IsCompact Set.range	—	image_uIcc Real.instIsOrderedAddMonoid Real.instArchimedean IsCompact.image isCompact_uIcc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal
isBounded_of_continuous 📖	mathematical	Function.Periodic Real Real.instAdd Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Bornology.IsBounded PseudoMetricSpace.toBornology Set.range	—	IsCompact.isBounded compact_of_continuous

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cobounded_eq 📖	mathematical	—	Bornology.cobounded Real PseudoMetricSpace.toBornology pseudoMetricSpace Filter Filter.instSup Filter.atBot instPreorder Filter.atTop	—	Metric.comap_dist_right_atTop sub_zero Filter.comap_abs_atTop instIsOrderedAddMonoid
continuous_inv 📖	mathematical	—	Continuous Real instZero instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instInv	—	ContinuousOn.restrict continuousOn_inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal
exists_seq_rat_strictAnti_tendsto 📖	mathematical	—	StrictAnti Nat.instPreorder Rat.instPreorder Real instLT instRatCast Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	—	DenseRange.exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Rat.denseRange_cast instArchimedean StrictMono.monotone Rat.cast_strictMono
exists_seq_rat_strictMono_tendsto 📖	mathematical	—	StrictMono Nat.instPreorder Rat.instPreorder Real instLT instRatCast Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	—	DenseRange.exists_seq_strictMono_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instNoMinOrderOfNontrivial instIsOrderedRing instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Rat.denseRange_cast instArchimedean StrictMono.monotone Rat.cast_strictMono
isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici 📖	mathematical	Filter.Tendsto Real Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace AntitoneOn instPreorder Set.Ici BddBelow instLE Set.image	IsGLB	—	tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici isGLB_csInf Set.image_nonempty Set.nonempty_Ici
isGLB_of_tendsto_antitone_bddBelow 📖	mathematical	Filter.Tendsto Real Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Antitone instPreorder BddBelow instLE Set.range	IsGLB	—	tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Filter.atTop_neBot tendsto_atTop_ciInf LinearOrder.infConvergenceClass isGLB_ciInf
isLUB_of_tendsto_monotoneOn_bddAbove_nat_Ici 📖	mathematical	Filter.Tendsto Real Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace MonotoneOn instPreorder Set.Ici BddAbove instLE Set.image	IsLUB	—	tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici isLUB_csSup Set.image_nonempty Set.nonempty_Ici
isLUB_of_tendsto_monotone_bddAbove 📖	mathematical	Filter.Tendsto Real Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Monotone instPreorder BddAbove instLE Set.range	IsLUB	—	tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Filter.atTop_neBot tendsto_atTop_ciSup LinearOrder.supConvergenceClass isLUB_ciSup
isTopologicalBasis_Ioo_rat 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Set.iUnion Set Set.instSingletonSet Set.Ioo instPreorder instRatCast	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds OrderTopology.to_orderClosedTopology instOrderTopologyReal mem_nhds_iff_exists_Ioo_subset instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial instNoMinOrderOfNontrivial IsOpen.mem_nhds exists_rat_btwn instIsStrictOrderedRing instArchimedean Rat.cast_lt LT.lt.trans
mem_closure_iff 📖	mathematical	—	Real Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instLT abs lattice instAddGroup instSub	—	mem_closure_iff_nhds_basis Metric.nhds_basis_ball
subfield_eq_of_closed 📖	mathematical	—	Top.top Subfield Real instDivisionRing Subfield.instTop	—	SetLike.ext'_iff Subfield.coe_top IsClosed.closure_eq Dense.closure_eq Dense.mono SubfieldClass.ratCast_mem Subfield.instSubfieldClass Rat.denseRange_cast instIsStrictOrderedRing instOrderTopologyReal instArchimedean
tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici 📖	mathematical	AntitoneOn Real Nat.instPreorder instPreorder Set.Ici BddBelow instLE Set.image	Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace InfSet.sInf instInfSet	—	Filter.tendsto_add_atTop_iff_nat Set.range_add_eq_image_Ici Nat.instCanonicallyOrderedAdd Nat.instOrderedSub sInf_range tendsto_atTop_ciInf LinearOrder.infConvergenceClass instOrderTopologyReal antitone_add_nat_iff_antitoneOn_nat_Ici Set.Ici.eq_1
tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici 📖	mathematical	MonotoneOn Real Nat.instPreorder instPreorder Set.Ici BddAbove instLE Set.image	Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SupSet.sSup instSupSet	—	Filter.tendsto_add_atTop_iff_nat Set.range_add_eq_image_Ici Nat.instCanonicallyOrderedAdd Nat.instOrderedSub sSup_range tendsto_atTop_ciSup LinearOrder.supConvergenceClass instOrderTopologyReal monotone_add_nat_iff_monotoneOn_nat_Ici Set.Ici.eq_1
totallyBounded_ball 📖	mathematical	—	TotallyBounded Real PseudoMetricSpace.toUniformSpace pseudoMetricSpace Metric.ball	—	ball_eq_Ioo totallyBounded_Ioo ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal
uniformContinuous_abs 📖	mathematical	—	UniformContinuous Real PseudoMetricSpace.toUniformSpace pseudoMetricSpace abs lattice instAddGroup	—	Metric.uniformContinuous_iff lt_of_le_of_lt abs_abs_sub_abs_le_abs_sub instIsOrderedAddMonoid
uniformContinuous_inv 📖	mathematical	Real instLT instZero instLE abs lattice instAddGroup	UniformContinuous Set.Elem instUniformSpaceSubtype Set Set.instMembership PseudoMetricSpace.toUniformSpace pseudoMetricSpace instInv	—	Metric.uniformContinuous_iff rat_inv_continuous_lemma instIsStrictOrderedRing IsAbsoluteValue.abs_isAbsoluteValue
uniformContinuous_mul 📖	mathematical	Real instLT abs lattice instAddGroup	UniformContinuous Set.Elem instUniformSpaceSubtype Set Set.instMembership instUniformSpaceProd PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul	—	Metric.uniformContinuous_iff rat_mul_continuous_lemma instIsStrictOrderedRing IsAbsoluteValue.abs_isAbsoluteValue max_lt_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_of_rat_image_lt 📖	mathematical	—	closure Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.image Real.instRatCast setOf Real.instLE	—	Set.ext Real.instIsStrictOrderedRing IsStrictOrderedRing.toCharZero closure_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_ordConnected_inter_rat Set.ordConnected_Ioi lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true AddLeftCancelSemigroup.toIsLeftCancelAdd
closure_ordConnected_inter_rat 📖	mathematical	Set.Nontrivial Real	closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set Set.instInter Set.range Real.instRatCast	—	HasSubset.Subset.antisymm Set.instAntisymmSubset closure_mono Set.inter_subset_left IsClosed.closure_subset_iff isClosed_closure Real.mem_closure_iff Set.Nontrivial.exists_ne Ne.lt_or_gt exists_rat_btwn Real.instIsStrictOrderedRing Real.instArchimedean max_lt sub_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.OrdConnected.out LT.lt.le max_lt_iff abs_sub_comm abs_of_pos sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add lt_min lt_add_of_pos_right lt_min_iff

---

← Back to Index