English
For Pi-indexed preorders with DecidableEq, a ⩿ b is equivalent to the existence of i and x such that a_i ⩿ x and b equals update a at i with x.
Русский
Для предмножества π с индексами и декидируемым равенством существует i и x такие, что a_i ⩿ x и b равняется обновлению a на i значением x.
LaTeX
$$$a ⩿ b \\iff \\exists i x, a_i ⩿ x \\land b = \\mathrm{Function.update}\\ a\\ i\\ x$$$
Lean4
theorem wcovBy_iff_exists_right_eq [Nonempty ι] [DecidableEq ι] : a ⩿ b ↔ ∃ i x, a i ⩿ x ∧ b = Function.update a i x :=
by
rw [wcovBy_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⟩
