dite_prop_iff_and

Mathlib.Logic.Basic

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

← MathLib Explorer

English

The dite P Q R is equivalent to (∀ h, Q h) ∧ (∀ h, R h).

Русский

Dite P Q R эквивалентно (∀ h, Q h) ∧ (∀ h, R h).

LaTeX

$$$\dite P Q R \iff \big(\forall h, Q h\big) \land \big(\forall h, R h\big)$$$

Lean4

theorem dite_prop_iff_and {Q : P → Prop} {R : ¬P → Prop} : dite P Q R ↔ (∀ h, Q h) ∧ (∀ h, R h) := by
  by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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