Theorems · Theorem · order theory
Set.Finite.biUnion
∀ {α : Type u} {ι : Type u_1} {s : Set ι}, s.Finite → ∀ {t : ι → Set α}, (∀ i ∈ s, (t i).Finite) → (⋃ i ∈ s, t i).Finite- Defined in
- Mathlib.Data.Set.Finite.Lattice
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.iUnionstatement · cited by 2,483
- Set.Finitestatement and proof · cited by 1,814
- Set.Finite.biUnion'proof · cited by 4
Cited by31
Results whose statement or proof uses this declaration.
- Set.Finite.preimage'proof · cited by 4
- Ideal.finite_setOfPred_absNorm_leproof · cited by 4
- LocallyFinite.finite_nonempty_inter_compactproof · cited by 4
- refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_setproof · cited by 3
- Polynomial.bUnion_roots_finiteproof · cited by 3
- Pell.exists_of_not_isSquareproof · cited by 3
- finprod_prod_commproof · cited by 3
- exists_covby_infinite_Ici_of_infinite_Iciproof · cited by 2
- Set.Finite.iUnionproof · cited by 2
- Ring.HasFiniteQuotients.finite_cardQuot_leproof · cited by 2
- finite_of_span_finite_eq_top_finsuppproof · cited by 2
- Rat.finite_rat_abs_sub_lt_one_div_den_sqproof · cited by 1