rel_imp — Mathlib

English

Implication is a congruence for Iff on both sides: if p ↔ p' and q ↔ q', then (p → q) ↔ (p' → q').

Русский

Импликация сохраняется под эквивалентностью: если p ↔ p' и q ↔ q', то (p → q) ↔ (p' → q').

LaTeX

$$$ (p \\leftrightarrow p') \\Rightarrow (q \\leftrightarrow q') \\Rightarrow (p \\rightarrow q) \\leftrightarrow (p' \\rightarrow q') $$$

Lean4

theorem rel_imp : (Iff ⇒ (Iff ⇒ Iff)) (· → ·) (· → ·) := fun _ _ h _ _ l => imp_congr h l

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