Theorems · Theorem · logic and foundations
Set.mem_inter
∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a → x ∈ b → x ∈ a ∩ b- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by25
Results whose statement or proof uses this declaration.
- MeasureTheory.hittingBtwn_leproof · cited by 8
- OpenPartialHomeomorph.contDiffAt_symmproof · cited by 3
- IsPreconnected.subset_of_closure_inter_subsetproof · cited by 3
- Dense.exists_seq_strictMono_tendsto_of_ltproof · cited by 3
- MeasureTheory.hittingBtwn_le_of_memproof · cited by 2
- MeasureTheory.hittingBtwn_mem_setproof · cited by 2
- connectedComponent_eq_iInter_isClopenproof · cited by 2
- CStarAlgebra.span_nonneg_inter_closedBallproof · cited by 2
- MeasureTheory.hittingAfter_le_of_memproof · cited by 2
- exists_countable_union_perfect_of_isClosedproof · cited by 1
- Set.vadd_inter_nonempty_iffproof · cited by 1