mem_toSubtype_iff — Mathlib

English

For p, f, a, b: b ∈ toSubtype p f a iff the underlying value equals f(a).

Русский

Для p, f, a, b: b ∈ toSubtype p f a тогда и только тогда, когда базовое значение равно f(a).

LaTeX

$$$$ b \in toSubtype(p,f)(a) \iff \uparrow b = f(a). $$$$

Lean4

theorem mem_toSubtype_iff {p : β → Prop} {f : α → β} {a : α} {b : Subtype p} : b ∈ toSubtype p f a ↔ ↑b = f a := by
  rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]

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