Theorems · Theorem · order theory

Set.range_quot_lift

∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {r : ι → ι → Prop} (hf : ∀ (x y : ι), r x y → f x = f y),
  Set.range (Quot.lift f hf) = Set.range f

Defined in

Mathlib.Data.Set.Image

Cited by

4 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext, Quot.sound