Dini

📁 Source: Mathlib/Topology/UniformSpace/Dini.lean

Statistics

Metric	Count
Definitions	0
Theorems tendstoLocallyUniformlyOn_of_forall_tendsto, tendstoLocallyUniformly_of_forall_tendsto, tendstoUniformlyOn_of_forall_tendsto, tendstoUniformly_of_forall_tendsto, tendsto_of_antitone_of_pointwise, tendsto_of_monotone_of_pointwise, tendstoLocallyUniformlyOn_of_forall_tendsto, tendstoLocallyUniformly_of_forall_tendsto, tendstoUniformlyOn_of_forall_tendsto, tendstoUniformly_of_forall_tendsto	10
Total	10

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendstoLocallyUniformlyOn_of_forall_tendsto 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoLocallyUniformlyOn	—	Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto OrderDual.instHasSolidNorm OrderDual.isOrderedAddMonoid ESeminormedAddCommMonoid.add_comm
tendstoLocallyUniformly_of_forall_tendsto 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Antitone Pi.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoLocallyUniformly	—	Monotone.tendstoLocallyUniformly_of_forall_tendsto OrderDual.instHasSolidNorm OrderDual.isOrderedAddMonoid ESeminormedAddCommMonoid.add_comm
tendstoUniformlyOn_of_forall_tendsto 📖	mathematical	IsCompact ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoUniformlyOn	—	Monotone.tendstoUniformlyOn_of_forall_tendsto OrderDual.instHasSolidNorm OrderDual.isOrderedAddMonoid ESeminormedAddCommMonoid.add_comm
tendstoUniformly_of_forall_tendsto 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Antitone Pi.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoUniformly	—	Monotone.tendstoUniformly_of_forall_tendsto OrderDual.instHasSolidNorm OrderDual.isOrderedAddMonoid ESeminormedAddCommMonoid.add_comm

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_of_antitone_of_pointwise 📖	mathematical	Antitone ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto DFunLike.coe instFunLike Filter.atTop nhds	compactOpen	—	tendsto_of_monotone_of_pointwise OrderDual.instHasSolidNorm OrderDual.isOrderedAddMonoid ESeminormedAddCommMonoid.add_comm
tendsto_of_monotone_of_pointwise 📖	mathematical	Monotone ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto DFunLike.coe instFunLike Filter.atTop nhds	compactOpen	—	tendsto_of_tendstoLocallyUniformly Monotone.tendstoLocallyUniformly_of_forall_tendsto continuous

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendstoLocallyUniformlyOn_of_forall_tendsto 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoLocallyUniformlyOn	—	tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe tendstoLocallyUniformly_of_forall_tendsto ContinuousOn.restrict
tendstoLocallyUniformly_of_forall_tendsto 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Monotone Pi.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoLocallyUniformly	—	Filter.eq_or_neBot Filter.bot_prod ge_of_tendsto instClosedIciTopology HasSolidNorm.orderClosedTopology Filter.mp_mem Filter.Ici_mem_atTop Filter.univ_mem' dist_eq_norm' Filter.Eventually.exists Filter.Tendsto.eventually eventually_lt_nhds instHasSolidNormReal Real.instIsOrderedAddMonoid IsOpen.mem_nhds isOpen_lt Continuous.norm Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_const Filter.eventually_ge_atTop LE.le.trans_lt norm_le_norm_of_abs_le_abs abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono sub_nonpos_of_le covariant_swap_add_of_covariant_add neg_sub
tendstoUniformlyOn_of_forall_tendsto 📖	mathematical	IsCompact ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoUniformlyOn	—	tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact tendstoLocallyUniformlyOn_of_forall_tendsto
tendstoUniformly_of_forall_tendsto 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Monotone Pi.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Filter.Tendsto Filter.atTop nhds	TendstoUniformly	—	tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace tendstoLocallyUniformly_of_forall_tendsto

---

← Back to Index