and_symm_right

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#and_symm_right

English

For α, a,b : α and p : Prop, p ∧ a = b ↔ p ∧ b = a.

Русский

Для типа α и элементов a,b : α, и пропозиции p, выполняется p ∧ (a = b) ↔ p ∧ (b = a).

LaTeX

$$$p \land (a = b) \\leftrightarrow p \\land (b = a)$$$

Lean4

theorem and_symm_right {α : Sort*} (a b : α) (p : Prop) : p ∧ a = b ↔ p ∧ b = a := by simp [eq_comm]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru