asSubtype_eq_of_mem — Mathlib

English

If y ∈ f x and x ∈ f.Dom, then f.asSubtype ⟨x, x ∈ f.Dom⟩ = y.

Русский

Если y ∈ f(x) и x ∈ Dom f, то f.asSubtype ⟨x, доказательство⟩ = y.

LaTeX

$$$\\text{If } f(x) \\text{ contains } y \\text{ and } x \\in \\mathrm{Dom}(f), \\text{ then } f.asSubtype(\\langle x, x \\in \\mathrm{Dom}(f) \\rangle) = y.$$$

Lean4

theorem asSubtype_eq_of_mem {f : α →. β} {x : α} {y : β} (fxy : y ∈ f x) (domx : x ∈ f.Dom) :
    f.asSubtype ⟨x, domx⟩ = y :=
  Part.mem_unique (Part.get_mem _) fxy

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