TuranDensity

📁 Source: Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean

Statistics

Metric	Count
Definitions turanDensity	1
Theorems antitoneOn_extremalNumber_div_choose_two, isEquivalent_extremalNumber, tendsto_turanDensity	3
Total	4

SimpleGraph

Definitions

Name	Category	Theorems
turanDensity 📖	CompOp	2 math math: tendsto_turanDensity, isEquivalent_extremalNumber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitoneOn_extremalNumber_div_choose_two 📖	mathematical	—	AntitoneOn Real Nat.instPreorder Real.instPreorder DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast extremalNumber Nat.choose Set.Ici	—	antitoneOn_nat_Ici_of_succ_le Fintype.card_fin div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Nat.choose_pos le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.cast_add Nat.cast_one extremalNumber_le_iff_of_nonneg mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_nonneg' mul_comm mul_div_assoc le_div_iff₀' Nat.cast_choose_two CharZero.NeZero.two Nat.cast_add_one add_sub_cancel_right mul_div mul_assoc mul_le_mul_iff_right₀ div_pos Nat.cast_pos' NeZero.charZero_one lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Nat.instIsStrictOrderedRing Nat.instNontrivial Real.instNontrivial Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_pred Nat.cast_mul Nat.cast_le Finset.card_univ Finset.card_nsmul_le_card_nsmul' Finset.bipartiteBelow.congr_simp Finset.filter_not Finset.filter_mem_eq_inter Finset.univ_inter Finset.card_compl card_toFinset_mem_edgeFinset edgeFinset_deleteIncidenceSet_eq_filter add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instIsOrderedAddMonoid card_edgeFinset_deleteIncidenceSet_le_extremalNumber
isEquivalent_extremalNumber 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Nat.instPreorder Real.instNatCast extremalNumber Real.instMul turanDensity Nat.choose	—	tendsto_turanDensity Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Asymptotics.isEquivalent_iff_tendsto_one one_mul div_mul_div_comm one_div_mul_cancel Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
tendsto_turanDensity 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast extremalNumber Nat.choose Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace turanDensity	—	tendsto_atTop_ciInf LinearOrder.infConvergenceClass instOrderTopologyReal antitone_add_nat_iff_antitoneOn_nat_Ici antitoneOn_extremalNumber_div_choose_two div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Filter.tendsto_add_atTop_iff_nat Filter.Tendsto.limUnder_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat

---

← Back to Index