kreplace_of_forall_not — Mathlib

English

If for all b: β a, the element ⟨a,b⟩ is not in l, then replacing a with b in l leaves l unchanged: kreplace a b l = l.

Русский

Если для всех b: β a элемент ⟨a,b⟩ отсутствует в l, то замена a на b в l не изменяет список: kreplace a b l = l.

LaTeX

$$$ \forall b:β a, \langle a,b\rangle \notin l \Rightarrow \ \mathrm{kreplace}(a,b,l) = l $$$

Lean4

theorem kreplace_of_forall_not (a : α) (b : β a) {l : List (Sigma β)} (H : ∀ b : β a, Sigma.mk a b ∉ l) :
    kreplace a b l = l :=
  lookmap_of_forall_not _ <| by grind

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