iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iff {S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {l : List α} : IsChain R l ↔ IsChain S l :=
  ⟨IsChain.imp fun a b => (H a b).1, IsChain.imp fun a b => (H a b).2⟩

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