val_mk — Mathlib

English

For x ∈ L with hx ∈ S, S.val ⟨x, hx⟩ = x; the embedding sends a representative to its underlying element.

Русский

Для x ∈ L с доказательством принадлежности hx ∈ S, S.val ⟨x, hx⟩ = x; вложение отправляет представителя в соответствующий элемент.

LaTeX

$$$ S.val(\\langle x, hx \\rangle) = x $$$

Lean4

@[simp]
theorem val_mk {x : L} (hx : x ∈ S) : S.val ⟨x, hx⟩ = x :=
  rfl

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