mem_piDiag — Mathlib

English

An element f belongs to the diagonal piDiag of s if and only if it is a constant function equal to some a ∈ s.

Русский

Элемент f принадлежит диагонали piDiag s тогда и только тогда, когда он является константной функцией, равной некоторому a ∈ s.

LaTeX

$$$ f \\in s.\\piDiag ι \\iff \\exists a \\in s, \\; \\text{const}_{ι} a = f. $$$

Lean4

@[simp]
theorem mem_piDiag : f ∈ s.piDiag ι ↔ ∃ a ∈ s, const ι a = f :=
  mem_image

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