rel_and — 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 \\land q) \\leftrightarrow (p' \\land q')) $$$

Lean4

theorem rel_and : ((· ↔ ·) ⇒ (· ↔ ·) ⇒ (· ↔ ·)) (· ∧ ·) (· ∧ ·) := fun _ _ h₁ _ _ h₂ => and_congr h₁ h₂

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