wcovBy_iff_exists_left_eq — Mathlib

English

With Nonempty ι and DecidableEq, a ⩿ b iff there exists i and x such that x ⩿ b_i and a equals update of b at i by x.

Русский

С непустым ι и DecidableEq, a ⩿ b тогда и только тогда, когда существует i и x такие, что x ⩿ b_i и a равно обновлению b по i значением x.

LaTeX

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

Lean4

theorem wcovBy_iff_exists_left_eq [Nonempty ι] [DecidableEq ι] : a ⩿ b ↔ ∃ i x, x ⩿ b i ∧ a = Function.update b i x :=
  by
  rw [wcovBy_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⟩

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