codRestrict_apply — Mathlib

English

Evaluating the restricted embedding yields a pair consisting of the image and the membership witness.

Русский

При вычислении ограниченного вложения получается пара: изображение и свидетелство принадлежности.

LaTeX

$$$ RelEmbedding.codRestrict\\; p\\; f\\; H\\; a = \\langle f\\,a, H\\, a \\rangle. $$$

Lean4

@[simp]
theorem codRestrict_apply (p) (f : r ↪r s) (H a) : RelEmbedding.codRestrict p f H a = ⟨f a, H a⟩ :=
  rfl

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