Lattice

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

Statistics

Metric	Count
Definitions ContinuousInf, ContinuousSup, Lattice, TopologicalLattice	4
Theorems finset_inf, finset_inf', finset_inf'_apply, finset_inf_apply, finset_sup, finset_sup', finset_sup'_apply, finset_sup_apply, inf, inf', sup, sup', finset_inf, finset_inf', finset_inf'_apply, finset_inf_apply, finset_sup, finset_sup', finset_sup'_apply, finset_sup_apply, inf, inf', sup, sup', continuous_inf, finset_inf, finset_inf', finset_inf'_apply, finset_inf_apply, finset_sup, finset_sup', finset_sup'_apply, finset_sup_apply, inf, inf', sup, sup', continuous_sup, finset_inf, finset_inf', finset_inf'_apply, finset_inf_apply, finset_sup, finset_sup', finset_sup'_apply, finset_sup_apply, inf, inf', sup, sup', finset_inf'_nhds, finset_inf'_nhds_apply, finset_inf_nhds, finset_inf_nhds_apply, finset_sup'_nhds, finset_sup'_nhds_apply, finset_sup_nhds, finset_sup_nhds_apply, inf_nhds, inf_nhds', sup_nhds, sup_nhds', topologicalLattice, continuousInf, continuousSup, topologicalLattice, toContinuousInf, toContinuousSup, continuous_inf, continuous_sup	70
Total	74

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finset_inf 📖	mathematical	Continuous	Continuous Finset.inf Pi.instSemilatticeInf Pi.instOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	continuous_iff_continuousAt ContinuousAt.finset_inf continuousAt
finset_inf' 📖	mathematical	Finset.Nonempty Continuous	Continuous Finset.inf' Pi.instSemilatticeInf	—	continuous_iff_continuousAt ContinuousAt.finset_inf' continuousAt
finset_inf'_apply 📖	mathematical	Finset.Nonempty Continuous	Continuous Finset.inf'	—	continuous_iff_continuousAt ContinuousAt.finset_inf'_apply continuousAt
finset_inf_apply 📖	mathematical	Continuous	Continuous Finset.inf	—	continuous_iff_continuousAt ContinuousAt.finset_inf_apply continuousAt
finset_sup 📖	mathematical	Continuous	Continuous Finset.sup Pi.instSemilatticeSup Pi.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	continuous_iff_continuousAt ContinuousAt.finset_sup continuousAt
finset_sup' 📖	mathematical	Finset.Nonempty Continuous	Continuous Finset.sup' Pi.instSemilatticeSup	—	continuous_iff_continuousAt ContinuousAt.finset_sup' continuousAt
finset_sup'_apply 📖	mathematical	Finset.Nonempty Continuous	Continuous Finset.sup'	—	continuous_iff_continuousAt ContinuousAt.finset_sup'_apply continuousAt
finset_sup_apply 📖	mathematical	Continuous	Continuous Finset.sup	—	continuous_iff_continuousAt ContinuousAt.finset_sup_apply continuousAt
inf 📖	mathematical	Continuous	Continuous	—	comp continuous_inf prodMk
inf' 📖	mathematical	Continuous	Continuous Pi.instMinForall_mathlib	—	inf
sup 📖	mathematical	Continuous	Continuous	—	comp continuous_sup prodMk
sup' 📖	mathematical	Continuous	Continuous Pi.instMaxForall_mathlib	—	sup

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finset_inf 📖	mathematical	ContinuousAt	ContinuousAt Finset.inf Pi.instSemilatticeInf Pi.instOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	finset_inf_apply
finset_inf' 📖	mathematical	Finset.Nonempty ContinuousAt	ContinuousAt Finset.inf' Pi.instSemilatticeInf	—	finset_inf'_apply
finset_inf'_apply 📖	mathematical	Finset.Nonempty ContinuousAt	ContinuousAt Finset.inf'	—	Filter.Tendsto.finset_inf'_nhds_apply
finset_inf_apply 📖	mathematical	ContinuousAt	ContinuousAt Finset.inf	—	Filter.Tendsto.finset_inf_nhds_apply
finset_sup 📖	mathematical	ContinuousAt	ContinuousAt Finset.sup Pi.instSemilatticeSup Pi.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	finset_sup_apply
finset_sup' 📖	mathematical	Finset.Nonempty ContinuousAt	ContinuousAt Finset.sup' Pi.instSemilatticeSup	—	finset_sup'_apply
finset_sup'_apply 📖	mathematical	Finset.Nonempty ContinuousAt	ContinuousAt Finset.sup'	—	Filter.Tendsto.finset_sup'_nhds_apply
finset_sup_apply 📖	mathematical	ContinuousAt	ContinuousAt Finset.sup	—	Filter.Tendsto.finset_sup_nhds_apply
inf 📖	mathematical	ContinuousAt	ContinuousAt	—	inf'
inf' 📖	mathematical	ContinuousAt	ContinuousAt Pi.instMinForall_mathlib	—	Filter.Tendsto.inf_nhds'
sup 📖	mathematical	ContinuousAt	ContinuousAt	—	sup'
sup' 📖	mathematical	ContinuousAt	ContinuousAt Pi.instMaxForall_mathlib	—	Filter.Tendsto.sup_nhds'

ContinuousInf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_inf 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	—

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finset_inf 📖	mathematical	ContinuousOn	ContinuousOn Finset.inf Pi.instSemilatticeInf Pi.instOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	ContinuousWithinAt.finset_inf
finset_inf' 📖	mathematical	Finset.Nonempty ContinuousOn	ContinuousOn Finset.inf' Pi.instSemilatticeInf	—	ContinuousWithinAt.finset_inf'
finset_inf'_apply 📖	mathematical	Finset.Nonempty ContinuousOn	ContinuousOn Finset.inf'	—	ContinuousWithinAt.finset_inf'_apply
finset_inf_apply 📖	mathematical	ContinuousOn	ContinuousOn Finset.inf	—	ContinuousWithinAt.finset_inf_apply
finset_sup 📖	mathematical	ContinuousOn	ContinuousOn Finset.sup Pi.instSemilatticeSup Pi.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	ContinuousWithinAt.finset_sup
finset_sup' 📖	mathematical	Finset.Nonempty ContinuousOn	ContinuousOn Finset.sup' Pi.instSemilatticeSup	—	ContinuousWithinAt.finset_sup'
finset_sup'_apply 📖	mathematical	Finset.Nonempty ContinuousOn	ContinuousOn Finset.sup'	—	ContinuousWithinAt.finset_sup'_apply
finset_sup_apply 📖	mathematical	ContinuousOn	ContinuousOn Finset.sup	—	ContinuousWithinAt.finset_sup_apply
inf 📖	mathematical	ContinuousOn	ContinuousOn	—	inf'
inf' 📖	mathematical	ContinuousOn	ContinuousOn Pi.instMinForall_mathlib	—	ContinuousWithinAt.inf'
sup 📖	mathematical	ContinuousOn	ContinuousOn	—	sup'
sup' 📖	mathematical	ContinuousOn	ContinuousOn Pi.instMaxForall_mathlib	—	ContinuousWithinAt.sup'

ContinuousSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_sup 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	—

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finset_inf 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Finset.inf Pi.instSemilatticeInf Pi.instOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	finset_inf_apply
finset_inf' 📖	mathematical	Finset.Nonempty ContinuousWithinAt	ContinuousWithinAt Finset.inf' Pi.instSemilatticeInf	—	finset_inf'_apply
finset_inf'_apply 📖	mathematical	Finset.Nonempty ContinuousWithinAt	ContinuousWithinAt Finset.inf'	—	Filter.Tendsto.finset_inf'_nhds_apply
finset_inf_apply 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Finset.inf	—	Filter.Tendsto.finset_inf_nhds_apply
finset_sup 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Finset.sup Pi.instSemilatticeSup Pi.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	finset_sup_apply
finset_sup' 📖	mathematical	Finset.Nonempty ContinuousWithinAt	ContinuousWithinAt Finset.sup' Pi.instSemilatticeSup	—	finset_sup'_apply
finset_sup'_apply 📖	mathematical	Finset.Nonempty ContinuousWithinAt	ContinuousWithinAt Finset.sup'	—	Filter.Tendsto.finset_sup'_nhds_apply
finset_sup_apply 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Finset.sup	—	Filter.Tendsto.finset_sup_nhds_apply
inf 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt	—	inf'
inf' 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Pi.instMinForall_mathlib	—	Filter.Tendsto.inf_nhds'
sup 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt	—	sup'
sup' 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Pi.instMaxForall_mathlib	—	Filter.Tendsto.sup_nhds'

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finset_inf'_nhds 📖	mathematical	Finset.Nonempty Filter.Tendsto nhds	Filter.Tendsto Finset.inf' Pi.instSemilatticeInf nhds	—	finset_sup'_nhds OrderDual.continuousSup
finset_inf'_nhds_apply 📖	mathematical	Finset.Nonempty Filter.Tendsto nhds	Filter.Tendsto Finset.inf' nhds	—	finset_sup'_nhds_apply OrderDual.continuousSup
finset_inf_nhds 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto Finset.inf Pi.instSemilatticeInf Pi.instOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder nhds	—	finset_sup_nhds OrderDual.continuousSup
finset_inf_nhds_apply 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto Finset.inf nhds	—	finset_sup_nhds_apply OrderDual.continuousSup
finset_sup'_nhds 📖	mathematical	Finset.Nonempty Filter.Tendsto nhds	Filter.Tendsto Finset.sup' Pi.instSemilatticeSup nhds	—	Finset.Nonempty.cons_induction Finset.singleton_nonempty Finset.cons_nonempty Finset.sup'_cons sup_nhds Finset.forall_mem_cons
finset_sup'_nhds_apply 📖	mathematical	Finset.Nonempty Filter.Tendsto nhds	Filter.Tendsto Finset.sup' nhds	—	finset_sup'_nhds
finset_sup_nhds 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto Finset.sup Pi.instSemilatticeSup Pi.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder nhds	—	Finset.eq_empty_or_nonempty Finset.sup_empty tendsto_const_nhds Finset.sup'_eq_sup finset_sup'_nhds
finset_sup_nhds_apply 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto Finset.sup nhds	—	finset_sup_nhds
inf_nhds 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto nhds	—	inf_nhds'
inf_nhds' 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto Pi.instMinForall_mathlib nhds	—	comp Continuous.tendsto continuous_inf prodMk_nhds
sup_nhds 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto nhds	—	sup_nhds'
sup_nhds' 📖	mathematical	Filter.Tendsto nhds	Filter.Tendsto Pi.instMaxForall_mathlib nhds	—	comp Continuous.tendsto continuous_sup prodMk_nhds

LinearOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalLattice 📖	mathematical	—	TopologicalLattice DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	continuous_min continuous_max

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousInf 📖	mathematical	—	ContinuousInf OrderDual instTopologicalSpace instMinOfMax	—	ContinuousSup.continuous_sup
continuousSup 📖	mathematical	—	ContinuousSup OrderDual instTopologicalSpace instMaxOfMin	—	ContinuousInf.continuous_inf
topologicalLattice 📖	mathematical	—	TopologicalLattice OrderDual instTopologicalSpace instLattice	—	continuousInf TopologicalLattice.toContinuousSup continuousSup TopologicalLattice.toContinuousInf

TopologicalLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousInf 📖	mathematical	—	ContinuousInf SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—
toContinuousSup 📖	mathematical	—	ContinuousSup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—

(root)

Definitions

Name	Category	Theorems
ContinuousInf 📖	CompData	4 math math: HasSolidNorm.continuousInf, TopologicalLattice.toContinuousInf, Topology.IsLower.toContinuousInf, OrderDual.continuousInf
ContinuousSup 📖	CompData	5 math math: TopologicalSpace.Closeds.instContinuousSup, Topology.IsUpper.toContinuousInf, HasSolidNorm.continuousSup, OrderDual.continuousSup, TopologicalLattice.toContinuousSup
Lattice 📖	CompData	—
TopologicalLattice 📖	CompData	3 math math: HasSolidNorm.toTopologicalLattice, OrderDual.topologicalLattice, LinearOrder.topologicalLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_inf 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	ContinuousInf.continuous_inf
continuous_sup 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	ContinuousSup.continuous_sup

---

← Back to Index