range_coe_subtype — Mathlib

English

For a predicate p on α, the range of the projection from Subtype p to α is {x | p x}.

Русский

Для предиката p на α образ проекции Subtype p на α равен {x | p x}.

LaTeX

$$$ \operatorname{range}(\operatorname{Subtype.val}) = \{ x \mid p x \} $$$

Lean4

/-- 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)`. -/
@[simp]
theorem range_coe_subtype {p : α → Prop} : range ((↑) : Subtype p → α) = {x | p x} :=
  range_coe

Похожие утверждения