Mathlib Map

Theorems · Theorem · order theory

Set.forall_mem_insert

∀ {α : Type u_1} {P : α → Prop} {a : α} {s : Set α}, (∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x
Defined in
Mathlib.Data.Set.Insert
Cited by
4 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Metric.AreSeparated.finite_iUnion_left_iff · cited by 3AreSeparated.finite_iUnio…Set.Finite.iInf_biSup_of_monotone · cited by 2Finite.iInf_biSup_of_mono…Set.Finite.iSup_biInf_of_monotone · cited by 2Finite.iSup_biInf_of_mono…Set.Finite.bddBelow_biUnion · cited by 0Finite.bddBelow_biUnionSet · cited by 53352SetSet.forall_mem_insertCITED BYCITES

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 by4

Results whose statement or proof uses this declaration.