Documentation Verification Report

Infinite

📁 Source: Mathlib/Order/Interval/Set/Infinite.lean

Statistics

Metric	Count
Definitions `Infinite`, `Infinite`, `Infinite`	3
Theorems `infinite`, `infinite`, `infinite`, `Icc_infinite`, `Ici_infinite`, `infinite`, `Ico_infinite`, `Iic_infinite`, `Iio_infinite`, `infinite`, `Ioc_infinite`, `Ioi_infinite`, `infinite`, `Ioo_infinite`, `instInfiniteElemIciOfNoMaxOrder`, `instInfiniteElemIicOfNoMinOrder`, `instInfiniteElemIioOfNoMinOrder`, `instInfiniteElemIoiOfNoMaxOrder`	18
Total	21

Hyperreal

Definitions

Name	Category	Theorems
`Infinite` 📖	MathDef	22 math math: `infinite_neg`, `not_infinite_of_exists_st`, `not_infinite_zero`, `infinite_abs_iff`, `not_infinite_iff_exist_lt_gt`, `infinite_iff_infinitesimal_inv`, `infinitePos_iff_infinite_and_pos`, `infiniteNeg_iff_infinite_and_neg`, `exists_st_iff_not_infinite`, `infinitePos_abs_iff_infinite_abs`, `IsSt.not_infinite`, `infiniteNeg_iff_infinite_of_neg`, `infinitePos_iff_infinite_of_pos`, `infinite_iff_not_exists_st`, `infinitesimal_iff_infinite_inv`, `infinitePos_iff_infinite_of_nonneg`, `infinite_iff_abs_lt_abs`, `infinite_omega`, `infinite_of_infinitesimal_inv`, `Infinitesimal.not_infinite`, `not_infinite_real`, `infinitePos_abs_iff_infinite`

NoMaxOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	—	`Infinite`	—	`Nat.exists_strictMono` `Infinite.of_injective` `instInfiniteNat` `StrictMono.injective`

NoMinOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	—	`Infinite`	—	`NoMaxOrder.infinite` `OrderDual.instNonempty` `OrderDual.noMaxOrder`

Set

Definitions

Name	Category	Theorems
`Infinite` 📖	MathDef	100 math math: `MeasurableSet.sep_infinite`, `Finite.not_infinite`, `bergelson`, `infinite_range_of_injective`, `Nat.infinite_setOf_prime_modEq_one`, `infinite_smul_set`, `Filter.frequently_cofinite_iff_infinite`, `Real.range_sin_infinite`, `infinite_of_not_bddAbove`, `infinite_not_isOfFinAddOrder`, `Matroid.RankInfinite.exists_infinite_isBase`, `Nat.infinite_deficient`, `infinite_of_mem_nhds`, `finite_or_infinite`, `Nat.infinite_setOf_prime`, `infinite_add`, `IsPreconnected.infinite_of_nontrivial`, `infinite_inv`, `Nat.infinite_odd_deficient`, `infinite_of_not_bddBelow`, `Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational`, `SimpleGraph.infinite_iff_in_eventualRange`, `Nat.frequently_atTop_iff_infinite`, `Nat.infinite_odd_abundant`, `infinite_prod`, `infinite_range_iff`, `MeasureTheory.Measure.count_apply_eq_top`, `infinite_sub`, `Filter.cofinite.limsup_set_eq`, `SimpleGraph.end_componentCompl_infinite`, `ProbabilityTheory.uniformOn_eq_zero`, `infinite_mul`, `infinite_zpowers`, `encard_eq_top_iff`, `infinite_not_isOfFinOrder`, `infinite_image2`, `Filter.cofinite_inf_principal_neBot_iff`, `Iio_infinite`, `not_finite`, `Nat.infinite_even_abundant`, `Infinite.of_accPt`, `Matroid.IsBase.diff_infinite_comm`, `Ioi_infinite`, `Module.infinite_range_reflection_reflection_iterate_iff`, `infinite_or_finite`, `bergelson'`, `infinite_coe_iff`, `Matroid.IsBase.infinite`, `MeasurableSet.setOf_infinite`, `exists_seq_infinite_isOpen_pairwise_disjoint`, `Nat.setOf_prime_and_eq_mod_infinite`, `infinite_zmultiples`, `Iic_infinite`, `infinite_multiples`, `Filter.frequently_cofinite_mem_iff_infinite`, `infinite_of_forall_exists_gt`, `not_infinite`, `infinite_vadd_set`, `infinite_of_forall_exists_lt`, `infinite_iUnion`, `FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize`, `Nat.infinite_setOf_pseudoprimes`, `infinite_of_finite_compl`, `Ioc_infinite`, `Nat.infinite_setOf_prime_and_modEq`, `countable_infinite_iff_nonempty_denumerable`, `infinite_univ`, `AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite`, `infinite_iff_exists_gt`, `infinite_of_injective_forall_mem`, `SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges`, `Nat.infinite_even_deficient`, `infinite_neg`, `Finite.infinite_compl`, `infinite_iff_tendsto_sum_indicator_atTop`, `Algebraic.infinite_of_charZero`, `infinite_iff_exists_lt`, `infinite_div`, `Ioo_infinite`, `infinite_image_iff`, `UnitAddCircle.mem_addWellApproximable_iff`, `Filter.cofinite.blimsup_set_eq`, `Ici_infinite`, `exists_infinite_discreteTopology`, `Matroid.rankInfinite_iff`, `Icc_infinite`, `MeasureTheory.Measure.count_apply_eq_top'`, `infinite_range_add_nsmul_iff`, `infinite_range_add_smul_iff`, `infinite_iff_infinite_of_encard_eq_encard`, `Monoid.exponent_eq_zero_iff_range_orderOf_infinite`, `Nat.infinite_setOf_prime_and_eq_mod`, `infinite_union`, `infinite_iff_frequently_cofinite`, `Real.range_cos_infinite`, `infinite_powers`, `Ico_infinite`, `Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational`, `infinite_univ_iff`, `ProbabilityTheory.uniformOn_eq_zero'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Icc`	—	`Infinite.mono` `Ioo_subset_Icc_self` `Ioo_infinite`
`Ici_infinite` 📖	mathematical	—	`Infinite` `Ici`	—	`infinite_coe_iff` `instInfiniteElemIciOfNoMaxOrder`
`Ico_infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Ico`	—	`Infinite.mono` `Ioo_subset_Ico_self` `Ioo_infinite`
`Iic_infinite` 📖	mathematical	—	`Infinite` `Iic`	—	`infinite_coe_iff` `instInfiniteElemIicOfNoMinOrder`
`Iio_infinite` 📖	mathematical	—	`Infinite` `Iio`	—	`infinite_coe_iff` `instInfiniteElemIioOfNoMinOrder`
`Ioc_infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Ioc`	—	`Infinite.mono` `Ioo_subset_Ioc_self` `Ioo_infinite`
`Ioi_infinite` 📖	mathematical	—	`Infinite` `Ioi`	—	`infinite_coe_iff` `instInfiniteElemIoiOfNoMaxOrder`
`Ioo_infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Ioo`	—	`infinite_coe_iff` `Ioo.infinite`
`instInfiniteElemIciOfNoMaxOrder` 📖	mathematical	—	`Infinite` `Elem` `Ici`	—	`NoMaxOrder.infinite` `nonempty_Ici_subtype` `instNoMaxOrderElemIci`
`instInfiniteElemIicOfNoMinOrder` 📖	mathematical	—	`Infinite` `Elem` `Iic`	—	`NoMinOrder.infinite` `nonempty_Iic_subtype` `instNoMinOrderElemIic`
`instInfiniteElemIioOfNoMinOrder` 📖	mathematical	—	`Infinite` `Elem` `Iio`	—	`NoMinOrder.infinite` `nonempty_Iio_subtype` `instNoMinOrderElemIio`
`instInfiniteElemIoiOfNoMaxOrder` 📖	mathematical	—	`Infinite` `Elem` `Ioi`	—	`NoMaxOrder.infinite` `nonempty_Ioi_subtype` `instNoMaxOrderElemIoi`

Set.Icc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Set.Elem` `Set.Icc`	—	`Set.infinite_coe_iff` `Set.Icc_infinite`

Set.Ico

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Set.Elem` `Set.Ico`	—	`Set.infinite_coe_iff` `Set.Ico_infinite`

Set.Ioc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Set.Elem` `Set.Ioc`	—	`Set.infinite_coe_iff` `Set.Ioc_infinite`

Set.Ioo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	`Preorder.toLT`	`Infinite` `Set.Elem` `Set.Ioo`	—	`NoMaxOrder.infinite` `Set.nonempty_Ioo_subtype` `instNoMaxOrderElemIoo`

(root)

Definitions

Name	Category	Theorems
`Infinite` 📖	CompData	99 math math: `Sum.infinite_of_left`, `WType.infinite_of_nonempty_of_isEmpty`, `Submodule.QuotientBot.infinite`, `CharZero.infinite`, `Set.Ioo.infinite`, `Infinite.of_injective`, `instInfiniteMultisetOfNonempty`, `AddSubgroup.index_eq_zero_iff_infinite`, `Function.infinite_of_left`, `NoMinOrder.infinite`, `Set.Icc.infinite`, `not_finite_iff_infinite`, `Sum.infinite_of_right`, `Set.instInfiniteElemIoiOfNoMaxOrder`, `Set.infinite_range_iff`, `Set.powersetCard.instInfinite`, `instInfiniteAdditive`, `FirstOrder.Language.model_infiniteTheory_iff`, `instInfinitePerm`, `Infinite.instSigmaOfNonempty`, `instInfiniteFreeAbelianGroupOfNonempty`, `Cardinal.infinite_iff`, `finite_or_infinite`, `Cardinal.aleph0_le_mk_iff`, `DihedralGroup.instInfiniteOfNatNat`, `instInfinitePLift`, `NontriviallyNormedField.infinite`, `Infinite.of_injective_to_set`, `ENat.card_eq_top`, `DFinsupp.infinite_of_left`, `Subgroup.index_eq_zero_iff_infinite`, `not_infinite_iff_finite`, `instInfiniteOption`, `Finsupp.infinite_of_left`, `Set.Ico.infinite`, `instInfiniteOfUncountable`, `FirstOrder.Language.ElementarilyEquivalent.infinite_iff`, `infinite_prod`, `Set.infinite_coe_iff`, `instInfiniteFreeAddGroupOfNonempty`, `instInfiniteMultiplicative`, `Prod.infinite_of_left`, `Set.Ioc.infinite`, `Finite.not_infinite`, `MvPolynomial.infinite_of_infinite`, `instInfiniteProdSubtypeCommute`, `SimpleGraph.instInfiniteColoringOfNonempty`, `infinite_sum`, `MvPolynomial.infinite_of_nonempty`, `String.infinite`, `FirstOrder.Language.ElementarilyEquivalent.infinite`, `Polynomial.infinite`, `Cardinal.exists_infinite_fiber`, `instInfiniteFreeCommRing`, `Pi.infinite_of_exists_right`, `DFinsupp.infinite_of_exists_right`, `Transcendental.infinite`, `Prod.infinite_of_right`, `FirstOrder.Language.instInfiniteOfModelDloOrderOfNonempty`, `ZMod.infinite`, `IsAlgClosed.instInfinite`, `Module.Free.infinite`, `Equiv.infinite_iff`, `nonempty_denumerable_iff`, `Function.infinite_of_right`, `PreconnectedSpace.infinite`, `EuclideanSpace.infinite`, `Set.instInfiniteElemIciOfNoMaxOrder`, `Set.instInfiniteElemIicOfNoMinOrder`, `instInfiniteFreeRing`, `Infinite.of_surjective_from_set`, `instInfiniteFreeAddMonoidOfNonempty`, `Infinite.set`, `UpperHalfPlane.instInfinite`, `Infinite.sigma_of_right`, `Pi.infinite_of_left`, `instInfiniteFreeMonoidOfNonempty`, `Infinite.of_not_fintype`, `Finite.exists_infinite_fiber`, `RootPairing.infinite_of_linearIndependent_coxeterWeight_four`, `Infinite.of_surjective`, `Field.infinite_emb_of_transcendental`, `Int.infinite`, `instInfiniteFinset`, `Denumerable.instInfinite`, `Finsupp.infinite_of_right`, `isEmpty_fintype`, `Set.Infinite.to_subtype`, `Nat.card_eq_zero`, `instInfiniteListOfNonempty`, `NoMaxOrder.infinite`, `instInfiniteNat`, `OnePoint.infinite`, `instInfiniteULift`, `Set.instInfiniteElemIioOfNoMinOrder`, `Set.infinite_univ_iff`, `instInfiniteFreeGroupOfNonempty`, `Algebra.Transcendental.infinite`, `Nat.Primes.infinite`

---

← Back to Index