Documentation Verification Report

ConditionallyCompleteOrder

📁 Source: Mathlib/Data/Int/ConditionallyCompleteOrder.lean

Statistics

Metric	Count
Definitions `instConditionallyCompleteLinearOrder`	1
Theorems `csInf_empty`, `csInf_eq_leastOfBdd`, `csInf_eq_least_of_bdd`, `csInf_mem`, `csInf_of_not_bddBelow`, `csInf_of_not_bdd_below`, `csSup_empty`, `csSup_eq_greatestOfBdd`, `csSup_eq_greatest_of_bdd`, `csSup_mem`, `csSup_of_not_bddAbove`, `csSup_of_not_bdd_above`	12
Total	13

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`csInf_empty` 📖	mathematical	—	`InfSet.sInf` `ConditionallyCompleteLattice.toInfSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Set` `Set.instEmptyCollection`	—	—
`csInf_eq_leastOfBdd` 📖	mathematical	`Set` `Set.instMembership`	`InfSet.sInf` `ConditionallyCompleteLattice.toInfSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `leastOfBdd`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `coe_leastOfBdd_eq`
`csInf_eq_least_of_bdd` 📖	mathematical	`Set` `Set.instMembership`	`InfSet.sInf` `ConditionallyCompleteLattice.toInfSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `leastOfBdd`	—	`csInf_eq_leastOfBdd`
`csInf_mem` 📖	mathematical	`Set.Nonempty` `BddBelow`	`Set` `Set.instMembership` `InfSet.sInf` `ConditionallyCompleteLattice.toInfSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder`	—	—
`csInf_of_not_bddBelow` 📖	mathematical	`BddBelow`	`InfSet.sInf` `ConditionallyCompleteLattice.toInfSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder`	—	—
`csInf_of_not_bdd_below` 📖	mathematical	`BddBelow`	`InfSet.sInf` `ConditionallyCompleteLattice.toInfSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder`	—	`csInf_of_not_bddBelow`
`csSup_empty` 📖	mathematical	—	`SupSet.sSup` `ConditionallyCompleteLattice.toSupSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Set` `Set.instEmptyCollection`	—	—
`csSup_eq_greatestOfBdd` 📖	mathematical	`Set` `Set.instMembership`	`SupSet.sSup` `ConditionallyCompleteLattice.toSupSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `greatestOfBdd`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `coe_greatestOfBdd_eq`
`csSup_eq_greatest_of_bdd` 📖	mathematical	`Set` `Set.instMembership`	`SupSet.sSup` `ConditionallyCompleteLattice.toSupSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `greatestOfBdd`	—	`csSup_eq_greatestOfBdd`
`csSup_mem` 📖	mathematical	`Set.Nonempty` `BddAbove`	`Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompleteLattice.toSupSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder`	—	—
`csSup_of_not_bddAbove` 📖	mathematical	`BddAbove`	`SupSet.sSup` `ConditionallyCompleteLattice.toSupSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder`	—	—
`csSup_of_not_bdd_above` 📖	mathematical	`BddAbove`	`SupSet.sSup` `ConditionallyCompleteLattice.toSupSet` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder`	—	`csSup_of_not_bddAbove`

(root)

Definitions

Name	Category	Theorems
`instConditionallyCompleteLinearOrder` 📖	CompOp	71 math math: `tendsto_zero_iff_meromorphicOrderAt_pos`, `EisensteinSeries.hasSum_e2Summand_symmetricIcc`, `RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root`, `Padic.withValUniformEquiv_norm_le_one_iff`, `tendsto_cobounded_iff_meromorphicOrderAt_neg`, `Int.padicValuation_lt_one_iff`, `MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt`, `Int.csInf_mem`, `RootPairing.coe_chainBotCoeff_eq_sSup`, `setOf_liouvilleWith_subset_aux`, `Set.Nonempty.eq_Icc_iff_int`, `RootPairing.setOf_root_add_zsmul_mem_eq_Icc`, `Int.csInf_eq_least_of_bdd`, `RootPairing.Base.pos_or_neg_of_sum_smul_root_mem`, `ValuativeRel.nonempty_orderIso_withZeroMul_int_iff`, `EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero`, `meromorphicOrderAt_add`, `EisensteinSeries.G2_eq_tsum_symmetricIco`, `Int.csSup_eq_greatestOfBdd`, `RootPairing.setOf_root_sub_zsmul_mem_eq_Icc`, `Int.cofinite_eq`, `tendsto_intCast_atBot_sup_atTop_cobounded`, `SummationFilter.hasSum_symmetricIoc_int_iff`, `AnalyticAt.meromorphicOrderAt_nonneg`, `Int.ball_eq_Ioo`, `EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero`, `SummationFilter.hasSum_symmetricIcc_iff`, `RootPairing.coe_chainTopCoeff_eq_sSup`, `Int.csInf_eq_leastOfBdd`, `RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent`, `Int.csInf_of_not_bddBelow`, `tendsto_nhds_iff_meromorphicOrderAt_nonneg`, `EisensteinSeries.hasSum_e2Summand_symmetricIco`, `Padic.AddValuation.map_add`, `meromorphicNFAt_iff_analyticAt_or`, `RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root`, `SummationFilter.hasProd_symmetricIco_int_iff`, `SummationFilter.hasSum_symmetricIco_int_iff`, `Int.csSup_of_not_bddAbove`, `Int.csSup_eq_greatest_of_bdd`, `EisensteinSeries.tsum_tsum_symmetricIco_sub_eq`, `RootPairing.Base.exists_root_eq_sum_int`, `RootPairing.root_add_zsmul_mem_range_iff`, `EisensteinSeries.tendsto_double_sum_S_act`, `SummationFilter.symmetricIcc_eq_symmetricIoo_int`, `Int.closedBall_eq_Icc`, `EisensteinSeries.summable_e2Summand_symmetricIcc`, `Int.csSup_mem`, `EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq`, `Padic.norm_rat_le_one_iff_padicValuation_le_one`, `EisensteinSeries.summable_e2Summand_symmetricIco`, `RootPairing.root_sub_zsmul_mem_range_iff`, `SummationFilter.symmetricIcc_eq_map_Icc_nat`, `tendsto_intCast_atTop_cobounded`, `SummationFilter.hasProd_symmetricIcc_iff`, `Int.csSup_of_not_bdd_above`, `Int.padicValuation_le_one`, `Int.instIsOrderBornology`, `ZLattice.sum_piFinset_Icc_rpow_le`, `tendsto_intCast_atBot_cobounded`, `Pell.IsFundamental.y_strictMono`, `SummationFilter.hasProd_symmetricIoc_int_iff`, `Int.csInf_of_not_bdd_below`, `EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act`, `Int.csSup_empty`, `ClassGroup.exists_mem_finset_approx'`, `ClassGroup.exists_mem_finsetApprox`, `Rat.padicValuation_le_one_iff`, `Int.cobounded_eq`, `Int.csInf_empty`, `EisensteinSeries.tsum_symmetricIco_tsum_sub_eq`

---

← Back to Index