Lemmas

📁 Source: Mathlib/Data/Set/Finite/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems fin_embedding, fin_param, induction_to, induction_to_univ, exists_lower_bound_image, exists_max_image, exists_min_image, exists_upper_bound_image, sUnion_finite_eq_univ	9
Total	9

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lower_bound_image 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eq_empty_or_nonempty exists_min_image
exists_max_image 📖	mathematical	Nonempty	Set instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Finset.exists_max_image Finite.mem_toFinset
exists_min_image 📖	mathematical	Nonempty	Set instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Finset.exists_min_image Finite.mem_toFinset
exists_upper_bound_image 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_lower_bound_image
sUnion_finite_eq_univ 📖	mathematical	—	sUnion setOf Set Finite univ	—	sUnion_eq_univ_iff finite_singleton

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fin_embedding 📖	mathematical	—	Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	Equiv.asEmbedding_range coe_toFinset
fin_param 📖	mathematical	—	Set.range	—	fin_embedding Function.Embedding.injective
induction_to 📖	—	Set Set.instHasSubset Set.instMembership Set.instSDiff Set.instInsert	—	—	to_subtype Finite.of_equiv Set.instFinite le_rfl WellFounded.induction_bot' IsWellFounded.wf Finite.to_wellFoundedGT ssubset_of_ne_of_subset Set.instIsNonstrictStrictOrderSubsetSSubset Set.instAntisymmSubset Set.insert_subset Set.ssubset_insert
induction_to_univ 📖	mathematical	Set Set.instMembership Set.instInsert	Set.univ	—	induction_to Set.finite_univ Set.subset_univ

---

← Back to Index