Mathlib Map

Theorems · Theorem · order theory

Finset.subset_inter

∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ u : Finset α}, s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u
Defined in
Mathlib.Data.Finset.Lattice.Basic
Cited by
3 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.

Finset.inter_nsmul_subset · cited by 0Finset.inter_nsmul_subsetFinset.inter_pow_subset · cited by 0Finset.inter_pow_subsetFinsupp.support_mul · cited by 0Finsupp.support_mulFinset · cited by 13712FinsetFinset.subset_interCITED BYCITES

Cites1

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

Cited by3

Results whose statement or proof uses this declaration.