PartialSups

📁 Source: Mathlib/Topology/Order/PartialSups.lean

Statistics

Metric	Count
Definitions	0
Theorems partialSups, partialSups_apply, partialSups, partialSups_apply, partialSups, partialSups_apply, partialSups, partialSups_apply, partialSups, partialSups_apply	10
Total	10

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups 📖	mathematical	Continuous	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Pi.instSemilatticeSup OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	continuous_iff_continuousAt ContinuousAt.partialSups continuousAt
partialSups_apply 📖	mathematical	Continuous	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	continuous_iff_continuousAt ContinuousAt.partialSups_apply continuousAt

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups 📖	mathematical	ContinuousAt	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Pi.instSemilatticeSup OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	partialSups_apply
partialSups_apply 📖	mathematical	ContinuousAt	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	Filter.Tendsto.partialSups_apply

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups 📖	mathematical	ContinuousOn	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Pi.instSemilatticeSup OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	ContinuousWithinAt.partialSups
partialSups_apply 📖	mathematical	ContinuousOn	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	ContinuousWithinAt.partialSups_apply

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups 📖	mathematical	ContinuousWithinAt	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Pi.instSemilatticeSup OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	partialSups_apply
partialSups_apply 📖	mathematical	ContinuousWithinAt	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	Filter.Tendsto.partialSups_apply

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partialSups 📖	mathematical	Filter.Tendsto nhds	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Pi.instSemilatticeSup OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	Finset.nonempty_range_add_one partialSups_eq_sup'_range finset_sup'_nhds
partialSups_apply 📖	mathematical	Filter.Tendsto nhds	DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	partialSups

---

← Back to Index