iff_of_mem_imp — Mathlib

English

If for all a,b in l, R a b ↔ S a b, then IsChain R l ↔ IsChain S l.

Русский

Если для всех a,b в l выполняется R a b ↔ S a b, то IsChain R l ↔ IsChain S l.

LaTeX

$$$ (\\forall a,b, a \\in l \\rightarrow b \\in l \\rightarrow (R(a,b) \\iff S(a,b))) \\Rightarrow IsChain\\;R\\;l \\iff IsChain\\;S\\;l $$$

Lean4

theorem iff_of_mem_imp {S : α → α → Prop} {l : List α} (H : ∀ a b : α, a ∈ l → b ∈ l → (R a b ↔ S a b)) :
    IsChain R l ↔ IsChain S l :=
  ⟨IsChain.imp_of_mem_imp (Iff.mp <| H · · · ·), IsChain.imp_of_mem_imp (Iff.mpr <| H · · · ·)⟩

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