covBy_iff_exists_right_eq — Mathlib

English

In Pi-types with DecidableEq, CovBy is equivalent to the existence of i and x such that a_i CovBy x and b equals update a at i with x.

Русский

Для типов Pi с DecidableEq CovBy эквивалентно существованию i и x such that a_i CovBy x и b равно обновлению a по i значением x.

LaTeX

$$$a \\CovBy b \\iff \\exists i x, a_i \\CovBy x ∧ b = \\mathrm{Function.update}\\ a i x$$$

Lean4

theorem covBy_iff_exists_right_eq [DecidableEq ι] : a ⋖ b ↔ ∃ i x, a i ⋖ x ∧ b = Function.update a i x :=
  by
  rw [covBy_iff]
  constructor
  · rintro ⟨i, hi, h⟩
    exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
  · rintro ⟨i, x, h, rfl⟩
    exact ⟨i, by simpa +contextual⟩

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