Mathlib Map

Theorems · Theorem · logic and foundations

Set.inter_subset_inter

∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ ∩ s₂ ⊆ t₁ ∩ t₂
Defined in
Mathlib.Data.Set.Basic
Cited by
66 results in Mathlib
Foundations
Depth 21 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.inter_subset_inter_left · cited by 36Set.inter_subset_inter_le…Set.inter_subset_inter_right · cited by 26Set.inter_subset_inter_ri…interior_inter · cited by 22interior_interLocallyFinite.subset · cited by 14LocallyFinite.subsetnhdsWithin_insert_of_ne · cited by 9nhdsWithin_insert_of_neHasMFDerivWithinAt.mono · cited by 9HasMFDerivWithinAt.monoFilter.push_pull · cited by 7Filter.push_pullMeasureTheory.measure_inter_add_sdiff₀ · cited by 6MeasureTheory.measure_int…Topology.IsInducing.locallyCompactSpace · cited by 4IsInducing.locallyCompact…tangentConeAt_closure · cited by 4tangentConeAt_closureFilter.HasBasis.inf' · cited by 3HasBasis.inf'MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists · cited by 3MeasureTheory.hittingBtwn…TopologicalSpace.Compacts.isPreconnected_nonempty_subsets · cited by 2Compacts.isPreconnected_n…MonotoneOn.exists_monotone_extension · cited by 2MonotoneOn.exists_monoton…HolderOnWith.hausdorffMeasure_image_le · cited by 2HolderOnWith.hausdorffMea…Set · cited by 53352Setinf_le_inf · cited by 54inf_le_infSet.inter_subset_interCITED BYCITES

Cites2

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
  • inf_le_infproof · cited by 54

Cited by66

Results whose statement or proof uses this declaration.