Mathlib Map

Theorems · Theorem · logic and foundations

PSet.mem_irrefl

∀ (x : PSet.{u_1}), x ∉ x
Defined in
Mathlib.SetTheory.ZFC.PSet
Cited by
1 results in Mathlib
Foundations
Depth 16 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PSet.not_subset_of_mem · cited by 1PSet.not_subset_of_memPSet · cited by 107PSetirrefl_of · cited by 8irrefl_ofPSet.mem_irreflCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PSetstatement and proof · cited by 107
  • irrefl_ofproof · cited by 8

Cited by1

Results whose statement or proof uses this declaration.