covBy_iff_exists_left_eq — Mathlib

English

With DecidableEq, CovBy is equivalent to the existence of i and x such that x CovBy b_i and a equals update of b at i by x.

Русский

С DecidableEq CovBy эквивалентно существованию i и x таких, что x CovBy b_i и a равно обновлению b по i значением x.

LaTeX

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

Lean4

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

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