wcovBy_iff — Mathlib

English

For nonempty index set ι, and DecidableEq ι, a ⩿ b iff there exists an index i and value x with a_i ⩿ x and b equals update a at i with x.

Русский

Для непустого множества индексов ι и разрешенного проверки равенства, a ⩿ b тогда и только тогда, когда существует индекс i и элемент x такие, что a_i ⩿ x и b совпадает с обновлением a на месте i значением x.

LaTeX

$$$a \\nsubeq b \\iff \\exists i x, a_i ⩿ x \\land b = \\mathrm{Function.update}\\ a\\ i\\ x$$$

Lean4

theorem wcovBy_iff [Nonempty ι] : a ⩿ b ↔ ∃ i, a i ⩿ b i ∧ ∀ j ≠ i, a j = b j := by simp [wcovBy_iff_antisymmRel]

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