mk_apply — Mathlib

English

The i-th coordinate of mk s x is given by the formula: (mk s x) i = if i ∈ s then x ⟨i, proof⟩ else 0.

Русский

i-я координата mk s x задается формулой: (mk s x) i = если i ∈ s, то x ⟨i, доказательство⟩, иначе 0.

LaTeX

$$$(\mathrm{mk}\ s\ x)\ i = \text{if } i \in s \text{ then } x\langle i, \text{proof} \rangle\ else\ 0$$$

Lean4

@[simp]
theorem mk_apply : (mk s x : ∀ i, β i) i = if H : i ∈ s then x ⟨i, H⟩ else 0 :=
  rfl

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