Mathlib Map

Theorems · Theorem · order theory

Finset.union_idempotent

∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∪ s = s
Defined in
Mathlib.Data.Finset.Lattice.Basic
Cited by
11 results in Mathlib
Foundations
Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEq
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NumberField.InfinitePlace.card_filter_mk_eq · cited by 3InfinitePlace.card_filter…Turing.PartrecToTM2.codeSupp_case · cited by 2PartrecToTM2.codeSupp_casemul_eq_mul_prime_prod · cited by 1mul_eq_mul_prime_prodFinset.powerset_sups_powerset_self · cited by 1Finset.powerset_sups_powe…Nat.primeFactors_pow_succ · cited by 1Nat.primeFactors_pow_succFinset.mulETransformLeft_one · cited by 0Finset.mulETransformLeft_…Finset.addETransformLeft_zero · cited by 0Finset.addETransformLeft_…Finset.addETransformRight_zero · cited by 0Finset.addETransformRight…Finset.mulETransformRight_one · cited by 0Finset.mulETransformRight…Finset.union_self · cited by 0Finset.union_selfFinset.four_functions_theorem · cited by 0Finset.four_functions_the…Finset · cited by 13712Finsetsup_idem · cited by 29sup_idemFinset.union_idempotentCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Finsetstatement and proof · cited by 13,712
  • sup_idemproof · cited by 29

Cited by11

Results whose statement or proof uses this declaration.