Mathlib Map

Theorems · Theorem · logic and foundations

ZFSet.mem_range_self

∀ {α : Type u_1} [inst : Small.{u, u_1} α] {f : α → ZFSet.{u}} (a : α), f a ∈ ZFSet.range f
Defined in
Mathlib.SetTheory.ZFC.Basic
Cited by
0 results in Mathlib
Foundations
Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Small
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Small · cited by 369SmallZFSet · cited by 259ZFSetZFSet.range · cited by 6ZFSet.rangeZFSet.mem_range_selfCITED BYCITES

Cites3

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

  • Smallstatement and proof · cited by 369
  • ZFSetstatement and proof · cited by 259
  • ZFSet.rangestatement · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.