Lattice

📁 Source: Mathlib/Data/Nat/Lattice.lean

Statistics

Metric	Count
Definitions `instConditionallyCompleteLinearOrderBot`, `instInfSet`, `instLattice`, `instSupSet`	4
Theorems `eq_Ici_of_nonempty_of_upward_closed`, `iInf_const_zero`, `iInf_le_succ`, `iInf_le_succ'`, `iInf_lt_succ`, `iInf_lt_succ'`, `iInf_of_empty`, `iSup_le_succ`, `iSup_le_succ'`, `iSup_lt_succ`, `iSup_lt_succ'`, `iSup_of_not_bddAbove`, `nonempty_of_pos_sInf`, `nonempty_of_sInf_eq_succ`, `notMem_of_lt_sInf`, `sInf_add`, `sInf_add'`, `sInf_def`, `sInf_empty`, `sInf_eq_zero`, `sInf_le`, `sInf_mem`, `sInf_upward_closed_eq_succ_iff`, `sSup_def`, `sSup_mem`, `sSup_of_not_bddAbove`, `sSup_eq_zero`, `biInter_le_succ`, `biInter_le_succ'`, `biInter_lt_succ`, `biInter_lt_succ'`, `biUnion_le_succ`, `biUnion_le_succ'`, `biUnion_lt_succ`, `biUnion_lt_succ'`	35
Total	39

Nat

Definitions

Name	Category	Theorems
`instConditionallyCompleteLinearOrderBot` 📖	CompOp	—
`instInfSet` 📖	CompOp	70 math math: `MeasureTheory.smul_le_stoppedValue_hittingBtwn`, `MeasureTheory.StronglyAdapted.isStoppingTime_upperCrossingTime`, `ENat.iInf_toNat`, `MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part`, `MeasureTheory.lowerCrossingTime_lt_upperCrossingTime`, `RingOfIntegers.exponent_eq_sInf`, `MeasureTheory.upcrossingsBefore_zero'`, `MeasureTheory.Submartingale.stoppedValue_leastGE`, `Pi.addOrderOf_eq_sInf`, `NNReal.natCast_iInf`, `sInf_eq_zero`, `SimpleGraph.Colorable.chromaticNumber_eq_sInf`, `MeasureTheory.integral_mul_upcrossingsBefore_le_integral`, `MeasureTheory.upperCrossingTime_bound_eq`, `nth_zero`, `MeasureTheory.crossing_pos_eq`, `SimpleGraph.dist_eq_sInf`, `sInf_mem`, `MeasureTheory.stoppedValue_lowerCrossingTime`, `MeasureTheory.upperCrossingTime_lt_lowerCrossingTime`, `MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le`, `Function.minimalPeriod_piMap`, `MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux`, `MeasureTheory.StronglyAdapted.measurable_upcrossings`, `MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le'`, `sInf_def`, `MeasureTheory.StronglyAdapted.isStoppingTime_crossing`, `MeasureTheory.stoppedValue_upperCrossingTime`, `MeasureTheory.smul_le_stoppedValue_hitting`, `ENat.coe_iInf`, `MeasureTheory.upperCrossingTime_lt_bddAbove`, `MeasureTheory.upcrossings_eq_top_of_frequently_lt`, `nth_eq_sInf`, `MeasureTheory.upperCrossingTime_lt_nonempty`, `MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing`, `MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le`, `MeasureTheory.upcrossingsBefore_le`, `MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part`, `ENat.coe_sInf`, `Pi.orderOf_eq_sInf`, `MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore`, `MeasureTheory.norm_stoppedValue_leastGE_le`, `Function.minimalPeriod_eq_sInf_n_pos_IsPeriodicPt`, `AddMonoid.exponent_eq_sInf`, `sInf_le`, `MeasureTheory.upcrossingsBefore_eq_sum`, `MeasureTheory.Submartingale.stoppedAbove`, `sInf_empty`, `sInf_upward_closed_eq_succ_iff`, `MeasureTheory.upcrossingsBefore_zero`, `MeasureTheory.upperCrossingTime_eq_of_bound_le`, `Monoid.exponent_eq_sInf`, `MeasureTheory.Submartingale.upcrossings_ae_lt_top'`, `iInf_of_empty`, `MeasureTheory.StronglyAdapted.isStoppingTime_lowerCrossingTime`, `eq_Ici_of_nonempty_of_upward_closed`, `MeasureTheory.StronglyAdapted.integrable_upcrossingsBefore`, `MeasureTheory.upperCrossingTime_lt_succ`, `MeasureTheory.stoppedAbove_le`, `Int.absNorm_under_eq_sInf`, `nth_count_eq_sInf`, `MeasureTheory.upcrossingsBefore_mono`, `MeasureTheory.mul_upcrossingsBefore_le`, `MeasureTheory.upcrossings_lt_top_iff`, `iInf_const_zero`, `MeasureTheory.upcrossingsBefore_pos_eq`, `Set.Nonempty.eq_Icc_iff_nat`, `MeasureTheory.exists_upperCrossingTime_eq`, `MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le'`, `Submodule.spanFinrank_eq_iInf`
`instLattice` 📖	CompOp	19 math math: `MonomialOrder.sPolynomial_leadingTerm_mul'`, `MvPolynomial.degreeOf_sum_le`, `MvPolynomial.totalDegree_eq`, `WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis`, `nilpotencyClass_pi`, `Multiset.uIcc_eq`, `MvPolynomial.weightedTotalDegree_one`, `MonomialOrder.sPolynomial_def`, `MvPolynomial.degreeOf_eq_sup`, `MonomialOrder.sPolynomial_monomial_mul`, `MonomialOrder.sPolynomial_monomial_mul'`, `MvPolynomial.totalDegree_finset_sum`, `MvPolynomial.weightedTotalDegree_rename_of_injective`, `MonomialOrder.degree_sPolynomial_le`, `MonomialOrder.coeff_sPolynomial_sup_eq_zero`, `MonomialOrder.degree_sPolynomial_lt_sup_degree`, `MonomialOrder.sPolynomial_mul_monomial`, `MonomialOrder.sPolynomial_leadingTerm_mul`, `MonomialOrder.degree_sPolynomial`
`instSupSet` 📖	CompOp	16 math math: `sSup_def`, `sSup_of_not_bddAbove`, `sSup_mem`, `ENat.coe_sSup`, `iSup_of_not_bddAbove`, `ENat.coe_iSup`, `AddMonoid.exponent_eq_iSup_addOrderOf`, `NNReal.natCast_iSup`, `Set.Infinite.Nat.sSup_eq_zero`, `Monoid.exponent_eq_iSup_orderOf`, `RootPairing.chainBotCoeff_eq_sSup`, `AddMonoid.exponent_eq_iSup_addOrderOf'`, `RootPairing.chainTopCoeff_eq_sSup`, `SSet.Subcomplex.Pairing.rank'_eq`, `Set.Nonempty.eq_Icc_iff_nat`, `Monoid.exponent_eq_iSup_orderOf'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_Ici_of_nonempty_of_upward_closed` 📖	mathematical	`Set.Nonempty` `Set` `Set.instMembership`	`Set.Ici` `instPreorder` `InfSet.sInf` `instInfSet`	—	`Set.ext` `sInf_le` `sInf_mem`
`iInf_const_zero` 📖	mathematical	—	`iInf` `instInfSet`	—	`isEmpty_or_nonempty` `iInf_of_empty` `sInf_eq_zero` `Set.range_const`
`iInf_le_succ` 📖	mathematical	—	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice`	—	`iSup_le_succ`
`iInf_le_succ'` 📖	mathematical	—	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice`	—	`iSup_le_succ'`
`iInf_lt_succ` 📖	mathematical	—	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice`	—	`iSup_lt_succ`
`iInf_lt_succ'` 📖	mathematical	—	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice`	—	`iSup_lt_succ'`
`iInf_of_empty` 📖	mathematical	—	`iInf` `instInfSet`	—	`iInf_of_isEmpty` `sInf_empty`
`iSup_le_succ` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`iSup_congr_Prop` `iSup_lt_succ`
`iSup_le_succ'` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`iSup_congr_Prop` `iSup_lt_succ'`
`iSup_lt_succ` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`iSup_congr_Prop` `biSup_le_eq_sup`
`iSup_lt_succ'` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`sup_iSup_nat_succ` `iSup_congr_Prop` `iSup_pos`
`iSup_of_not_bddAbove` 📖	mathematical	`BddAbove` `Set.range`	`iSup` `instSupSet`	—	`sSup_of_not_bddAbove`
`nonempty_of_pos_sInf` 📖	mathematical	`InfSet.sInf` `instInfSet`	`Set.Nonempty`	—	`sInf_eq_zero` `Set.not_nonempty_iff_eq_empty`
`nonempty_of_sInf_eq_succ` 📖	mathematical	`InfSet.sInf` `instInfSet`	`Set.Nonempty`	—	`nonempty_of_pos_sInf`
`notMem_of_lt_sInf` 📖	mathematical	`InfSet.sInf` `instInfSet`	`Set` `Set.instMembership`	—	`Set.eq_empty_or_nonempty` `Set.notMem_empty` `find_min` `sInf_def`
`sInf_add` 📖	—	`InfSet.sInf` `instInfSet` `setOf`	—	—	`Set.eq_empty_or_nonempty` `sInf_empty` `zero_add` `LE.le.eq_or_lt` `csInf_mem` `instWellFoundedLTNat` `nonempty_of_pos_sInf` `LE.le.trans_lt` `Eq.subset` `Set.instReflSubset` `sInf_def` `find_add`
`sInf_add'` 📖	—	`InfSet.sInf` `instInfSet` `setOf`	—	—	`nonempty_of_pos_sInf` `le_csInf` `le_of_not_gt` `notMem_of_lt_sInf` `LT.lt.le` `sInf_add`
`sInf_def` 📖	mathematical	`Set.Nonempty`	`InfSet.sInf` `instInfSet` `find` `Set` `Set.instMembership`	—	—
`sInf_empty` 📖	mathematical	—	`InfSet.sInf` `instInfSet` `Set` `Set.instEmptyCollection`	—	`sInf_eq_zero`
`sInf_eq_zero` 📖	mathematical	—	`InfSet.sInf` `instInfSet` `Set` `Set.instMembership` `Set.instEmptyCollection`	—	`Set.eq_empty_or_nonempty` `find.congr_simp` `sInf_def` `Set.Nonempty.ne_empty`
`sInf_le` 📖	mathematical	`Set` `Set.instMembership`	`InfSet.sInf` `instInfSet`	—	`sInf_def` `find_min'`
`sInf_mem` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `InfSet.sInf` `instInfSet`	—	`sInf_def` `find_spec`
`sInf_upward_closed_eq_succ_iff` 📖	mathematical	`Set` `Set.instMembership`	`InfSet.sInf` `instInfSet`	—	`eq_Ici_of_nonempty_of_upward_closed` `nonempty_of_sInf_eq_succ` `Set.mem_Ici` `le_rfl` `sInf_def` `find_eq_iff`
`sSup_def` 📖	mathematical	—	`SupSet.sSup` `instSupSet` `find`	—	—
`sSup_mem` 📖	mathematical	`Set.Nonempty` `BddAbove`	`Set` `Set.instMembership` `SupSet.sSup` `instSupSet`	—	`Set.Nonempty.csSup_mem` `Set.Finite.subset` `Set.finite_le_nat`
`sSup_of_not_bddAbove` 📖	mathematical	`BddAbove`	`SupSet.sSup` `instSupSet`	—	`Set.Infinite.Nat.sSup_eq_zero` `Set.infinite_of_not_bddAbove` `SemilatticeSup.instIsDirectedOrder`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_le_succ` 📖	mathematical	—	`iInter` `Set` `instInter`	—	`Nat.iInf_le_succ`
`biInter_le_succ'` 📖	mathematical	—	`iInter` `Set` `instInter`	—	`Nat.iInf_le_succ'`
`biInter_lt_succ` 📖	mathematical	—	`iInter` `Set` `instInter`	—	`Nat.iInf_lt_succ`
`biInter_lt_succ'` 📖	mathematical	—	`iInter` `Set` `instInter`	—	`Nat.iInf_lt_succ'`
`biUnion_le_succ` 📖	mathematical	—	`iUnion` `Set` `instUnion`	—	`Nat.iSup_le_succ`
`biUnion_le_succ'` 📖	mathematical	—	`iUnion` `Set` `instUnion`	—	`Nat.iSup_le_succ'`
`biUnion_lt_succ` 📖	mathematical	—	`iUnion` `Set` `instUnion`	—	`Nat.iSup_lt_succ`
`biUnion_lt_succ'` 📖	mathematical	—	`iUnion` `Set` `instUnion`	—	`Nat.iSup_lt_succ'`

Set.Infinite.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sSup_eq_zero` 📖	mathematical	`Set.Infinite`	`SupSet.sSup` `Nat.instSupSet`	—	`Set.Infinite.exists_gt` `LE.le.not_gt`

---

← Back to Index