rel_or — Mathlib

English

Let p, p', q, q' be propositions with p ↔ p' and q ↔ q'. Then (p ∨ q) ↔ (p' ∨ q').

Русский

Пусть p, p', q, q' — утверждения, причём p ↔ p' и q ↔ q'. Тогда (p ∨ q) ↔ (p' ∨ q').

LaTeX

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

Lean4

theorem rel_or : ((· ↔ ·) ⇒ (· ↔ ·) ⇒ (· ↔ ·)) (· ∨ ·) (· ∨ ·) := fun _ _ h₁ _ _ h₂ => or_congr h₁ h₂

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