KonigLemma

📁 Source: Mathlib/Order/KonigLemma.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_nat_orderEmbedding_of_forall_covby_finite, exists_orderEmbedding_covby_of_forall_covby_finite, exists_orderEmbedding_covby_of_forall_covby_finite_of_bot, exists_seq_covby_of_forall_covby_finite, exists_seq_forall_proj_of_forall_finite	5
Total	5

GradeMinOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nat_orderEmbedding_of_forall_covby_finite 📖	mathematical	Set.Finite setOf CovBy Preorder.toLT PartialOrder.toPreorder	DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding Bot.bot OrderBot.toBot grade Nat.instPreorder toGradeOrder	—	exists_orderEmbedding_covby_of_forall_covby_finite_of_bot grade_bot Nat.instNoMaxOrder CovBy.grade

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_orderEmbedding_covby_of_forall_covby_finite 📖	mathematical	Set.Finite setOf CovBy Preorder.toLT PartialOrder.toPreorder Set.Infinite Set.Ici	DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding	—	exists_seq_covby_of_forall_covby_finite strictMono_nat_of_lt_succ CovBy.lt
exists_orderEmbedding_covby_of_forall_covby_finite_of_bot 📖	mathematical	Set.Finite setOf CovBy Preorder.toLT PartialOrder.toPreorder	DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding Bot.bot OrderBot.toBot	—	exists_orderEmbedding_covby_of_forall_covby_finite Set.Ici_bot Set.infinite_univ
exists_seq_covby_of_forall_covby_finite 📖	—	Set.Finite setOf CovBy Preorder.toLT PartialOrder.toPreorder Set.Infinite Set.Ici	—	—	exists_covby_infinite_Ici_of_infinite_Ici
exists_seq_forall_proj_of_forall_finite 📖	—	Eq.le Nat.instPreorder LE.le.trans Set.Finite setOf	—	—	Eq.le LE.le.trans LE.le.antisymm LE.le.lt_of_ne IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd zero_le Finite.exists_infinite_fiber Infinite.instSigmaOfNonempty instInfiniteNat Set.Infinite.mono Set.infinite_coe_iff Set.Finite.subset Set.Finite.image exists_orderEmbedding_covby_of_forall_covby_finite OrderEmbedding.monotone

---

← Back to Index