Mathlib Map

Theorems · Theorem · logic and foundations

Set.Nonempty.right

∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty → t.Nonempty
Defined in
Mathlib.Data.Set.Basic
Cited by
5 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsPreconnected.preperfect_of_nontrivial · cited by 2IsPreconnected.preperfect…IsPreirreducible.of_subset_iUnion · cited by 1IsPreirreducible.of_subse…IsPiSystem.biInter_mem · cited by 1IsPiSystem.biInter_memMeasureTheory.Measure.nonempty_support · cited by 1Measure.nonempty_supportcsInf_le_csSup_of_nonempty_inter · cited by 0csInf_le_csSup_of_nonempt…Set · cited by 53352SetSet.Nonempty · cited by 2627Set.NonemptyNonempty.rightCITED 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
  • Set.Nonemptystatement and proof · cited by 2,627

Cited by5

Results whose statement or proof uses this declaration.