Theorems · Theorem · order theory

Subtype.range_coe_subtype

∀ {α : Type u_1} {p : α → Prop}, Set.range Subtype.val = {x | p x}

We make this the simp lemma instead of range_coe. The reason is that if we write for s : Set α the function (↑) : s → α, then the inferred implicit arguments of (↑) are ↑α (fun x ↦ x ∈ s).

Defined in

Mathlib.Data.Set.Image

Cited by

170 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 77 definitions · uses propext, Classical.choice, Quot.sound