Documentation Verification Report

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`	`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`	`Finset.inf'` `Pi.instSemilatticeInf`	—	`continuous_iff_continuousAt` `ContinuousAt.finset_inf'` `continuousAt`
`finset_inf'_apply` 📖	mathematical	`Finset.Nonempty` `Continuous`	`Finset.inf'`	—	`continuous_iff_continuousAt` `ContinuousAt.finset_inf'_apply` `continuousAt`
`finset_inf_apply` 📖	mathematical	`Continuous`	`Finset.inf`	—	`continuous_iff_continuousAt` `ContinuousAt.finset_inf_apply` `continuousAt`
`finset_sup` 📖	mathematical	`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`	`Finset.sup'` `Pi.instSemilatticeSup`	—	`continuous_iff_continuousAt` `ContinuousAt.finset_sup'` `continuousAt`
`finset_sup'_apply` 📖	mathematical	`Finset.Nonempty` `Continuous`	`Finset.sup'`	—	`continuous_iff_continuousAt` `ContinuousAt.finset_sup'_apply` `continuousAt`
`finset_sup_apply` 📖	mathematical	`Continuous`	`Finset.sup`	—	`continuous_iff_continuousAt` `ContinuousAt.finset_sup_apply` `continuousAt`
`inf` 📖	—	`Continuous`	—	—	`comp` `continuous_inf` `prodMk`
`inf'` 📖	mathematical	`Continuous`	`Pi.instMinForall_mathlib`	—	`inf`
`sup` 📖	—	`Continuous`	—	—	`comp` `continuous_sup` `prodMk`
`sup'` 📖	mathematical	`Continuous`	`Pi.instMaxForall_mathlib`	—	`sup`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finset_inf` 📖	mathematical	`ContinuousAt`	`Finset.inf` `Pi.instSemilatticeInf` `Pi.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`finset_inf_apply`
`finset_inf'` 📖	mathematical	`Finset.Nonempty` `ContinuousAt`	`Finset.inf'` `Pi.instSemilatticeInf`	—	`finset_inf'_apply`
`finset_inf'_apply` 📖	mathematical	`Finset.Nonempty` `ContinuousAt`	`Finset.inf'`	—	`Filter.Tendsto.finset_inf'_nhds_apply`
`finset_inf_apply` 📖	mathematical	`ContinuousAt`	`Finset.inf`	—	`Filter.Tendsto.finset_inf_nhds_apply`
`finset_sup` 📖	mathematical	`ContinuousAt`	`Finset.sup` `Pi.instSemilatticeSup` `Pi.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`finset_sup_apply`
`finset_sup'` 📖	mathematical	`Finset.Nonempty` `ContinuousAt`	`Finset.sup'` `Pi.instSemilatticeSup`	—	`finset_sup'_apply`
`finset_sup'_apply` 📖	mathematical	`Finset.Nonempty` `ContinuousAt`	`Finset.sup'`	—	`Filter.Tendsto.finset_sup'_nhds_apply`
`finset_sup_apply` 📖	mathematical	`ContinuousAt`	`Finset.sup`	—	`Filter.Tendsto.finset_sup_nhds_apply`
`inf` 📖	—	`ContinuousAt`	—	—	`inf'`
`inf'` 📖	mathematical	`ContinuousAt`	`Pi.instMinForall_mathlib`	—	`Filter.Tendsto.inf_nhds'`
`sup` 📖	—	`ContinuousAt`	—	—	`sup'`
`sup'` 📖	mathematical	`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`	`Finset.inf` `Pi.instSemilatticeInf` `Pi.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`ContinuousWithinAt.finset_inf`
`finset_inf'` 📖	mathematical	`Finset.Nonempty` `ContinuousOn`	`Finset.inf'` `Pi.instSemilatticeInf`	—	`ContinuousWithinAt.finset_inf'`
`finset_inf'_apply` 📖	mathematical	`Finset.Nonempty` `ContinuousOn`	`Finset.inf'`	—	`ContinuousWithinAt.finset_inf'_apply`
`finset_inf_apply` 📖	mathematical	`ContinuousOn`	`Finset.inf`	—	`ContinuousWithinAt.finset_inf_apply`
`finset_sup` 📖	mathematical	`ContinuousOn`	`Finset.sup` `Pi.instSemilatticeSup` `Pi.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`ContinuousWithinAt.finset_sup`
`finset_sup'` 📖	mathematical	`Finset.Nonempty` `ContinuousOn`	`Finset.sup'` `Pi.instSemilatticeSup`	—	`ContinuousWithinAt.finset_sup'`
`finset_sup'_apply` 📖	mathematical	`Finset.Nonempty` `ContinuousOn`	`Finset.sup'`	—	`ContinuousWithinAt.finset_sup'_apply`
`finset_sup_apply` 📖	mathematical	`ContinuousOn`	`Finset.sup`	—	`ContinuousWithinAt.finset_sup_apply`
`inf` 📖	—	`ContinuousOn`	—	—	`inf'`
`inf'` 📖	mathematical	`ContinuousOn`	`Pi.instMinForall_mathlib`	—	`ContinuousWithinAt.inf'`
`sup` 📖	—	`ContinuousOn`	—	—	`sup'`
`sup'` 📖	mathematical	`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`	`Finset.inf` `Pi.instSemilatticeInf` `Pi.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`finset_inf_apply`
`finset_inf'` 📖	mathematical	`Finset.Nonempty` `ContinuousWithinAt`	`Finset.inf'` `Pi.instSemilatticeInf`	—	`finset_inf'_apply`
`finset_inf'_apply` 📖	mathematical	`Finset.Nonempty` `ContinuousWithinAt`	`Finset.inf'`	—	`Filter.Tendsto.finset_inf'_nhds_apply`
`finset_inf_apply` 📖	mathematical	`ContinuousWithinAt`	`Finset.inf`	—	`Filter.Tendsto.finset_inf_nhds_apply`
`finset_sup` 📖	mathematical	`ContinuousWithinAt`	`Finset.sup` `Pi.instSemilatticeSup` `Pi.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`finset_sup_apply`
`finset_sup'` 📖	mathematical	`Finset.Nonempty` `ContinuousWithinAt`	`Finset.sup'` `Pi.instSemilatticeSup`	—	`finset_sup'_apply`
`finset_sup'_apply` 📖	mathematical	`Finset.Nonempty` `ContinuousWithinAt`	`Finset.sup'`	—	`Filter.Tendsto.finset_sup'_nhds_apply`
`finset_sup_apply` 📖	mathematical	`ContinuousWithinAt`	`Finset.sup`	—	`Filter.Tendsto.finset_sup_nhds_apply`
`inf` 📖	—	`ContinuousWithinAt`	—	—	`inf'`
`inf'` 📖	mathematical	`ContinuousWithinAt`	`Pi.instMinForall_mathlib`	—	`Filter.Tendsto.inf_nhds'`
`sup` 📖	—	`ContinuousWithinAt`	—	—	`sup'`
`sup'` 📖	mathematical	`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`	`Finset.inf'` `Pi.instSemilatticeInf`	—	`finset_sup'_nhds` `OrderDual.continuousSup`
`finset_inf'_nhds_apply` 📖	mathematical	`Finset.Nonempty` `Filter.Tendsto` `nhds`	`Finset.inf'`	—	`finset_sup'_nhds_apply` `OrderDual.continuousSup`
`finset_inf_nhds` 📖	mathematical	`Filter.Tendsto` `nhds`	`Finset.inf` `Pi.instSemilatticeInf` `Pi.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`finset_sup_nhds` `OrderDual.continuousSup`
`finset_inf_nhds_apply` 📖	mathematical	`Filter.Tendsto` `nhds`	`Finset.inf`	—	`finset_sup_nhds_apply` `OrderDual.continuousSup`
`finset_sup'_nhds` 📖	mathematical	`Finset.Nonempty` `Filter.Tendsto` `nhds`	`Finset.sup'` `Pi.instSemilatticeSup`	—	`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`	`Finset.sup'`	—	`finset_sup'_nhds`
`finset_sup_nhds` 📖	mathematical	`Filter.Tendsto` `nhds`	`Finset.sup` `Pi.instSemilatticeSup` `Pi.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`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`	`Finset.sup`	—	`finset_sup_nhds`
`inf_nhds` 📖	—	`Filter.Tendsto` `nhds`	—	—	`inf_nhds'`
`inf_nhds'` 📖	mathematical	`Filter.Tendsto` `nhds`	`Pi.instMinForall_mathlib`	—	`comp` `Continuous.tendsto` `continuous_inf` `prodMk_nhds`
`sup_nhds` 📖	—	`Filter.Tendsto` `nhds`	—	—	`sup_nhds'`
`sup_nhds'` 📖	mathematical	`Filter.Tendsto` `nhds`	`Pi.instMaxForall_mathlib`	—	`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` `instInf`	—	`ContinuousSup.continuous_sup`
`continuousSup` 📖	mathematical	—	`ContinuousSup` `OrderDual` `instTopologicalSpace` `instSup`	—	`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