Mathlib Map

Theorems · Theorem · order theory

Set.finite_iUnion

∀ {α : Type u} {ι : Sort w} [Finite ι] {f : ι → Set α}, (∀ (i : ι), (f i).Finite) → (⋃ i, f i).Finite
Defined in
Mathlib.Data.Set.Finite.Lattice
Cited by
14 results in Mathlib
Foundations
Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Finite
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.Finite.biUnion' · cited by 4Finite.biUnion'Filter.totallyBounded_iSup · cited by 2Filter.totallyBounded_iSupAlgebra.Presentation.finite_coeffs · cited by 1Presentation.finite_coeffsFormalMultilinearSeries.changeOrigin_eval_of_finite · cited by 1FormalMultilinearSeries.c…NumberField.finite_setOfPred_mulHeight₁_le · cited by 1NumberField.finite_setOfP…Matroid.IsRkFinite.iUnion · cited by 0IsRkFinite.iUnionFunction.HasFiniteMulSupport.iInf · cited by 0HasFiniteMulSupport.iInfIntermediateField.fg_iSup · cited by 0IntermediateField.fg_iSupFunction.HasFiniteMulSupport.iSup · cited by 0HasFiniteMulSupport.iSupFunction.HasFiniteSupport.iInf · cited by 0HasFiniteSupport.iInfFunction.HasFiniteSupport.iSup · cited by 0HasFiniteSupport.iSupFunction.HasFiniteMulSupport.pi · cited by 0HasFiniteMulSupport.piSubmodule.fg_pi · cited by 0Submodule.fg_piFunction.HasFiniteSupport.pi · cited by 0HasFiniteSupport.piSet · cited by 53352SetFinite · cited by 3029FiniteSet.iUnion · cited by 2483Set.iUnionSet.Finite · cited by 1814Set.FiniteSet.toFinite · cited by 174Set.toFiniteSet.finite_iUnionCITED BYCITES

Cites5

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
  • Finitestatement and proof · cited by 3,029
  • Set.iUnionstatement and proof · cited by 2,483
  • Set.Finitestatement and proof · cited by 1,814
  • Set.toFiniteproof · cited by 174

Cited by14

Results whose statement or proof uses this declaration.