sup_himp_distrib

Mathlib.Order.Heyting.Basic

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

← MathLib Explorer

English

For all a, b, c in α, a ∨ b → c = (a → c) ∧ (b → c).

Русский

Для любых a, b, c ∈ α выполняется (a ∨ b) ⇨ c = (a ⇨ c) ∧ (b ⇨ c).

LaTeX

$$$ (a \lor b) \to c = (a \to c) \wedge (b \to c) $$$

Lean4

theorem sup_himp_distrib (a b c : α) : a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c) :=
  eq_of_forall_le_iff fun d => by
    rw [le_inf_iff, le_himp_comm, sup_le_iff]
    simp_rw [le_himp_comm]

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

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

Разделы

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

Аффилиация

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