boundary_le_boundary_sup_sup_boundary_inf_right

Mathlib.Order.Heyting.Boundary

URI: https://scilib.ai/kg/mathlib#Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right

← MathLib Explorer

English

For all a,b, ∂ b ≤ ∂(a ⊔ b) ⊔ ∂(a ⊓ b).

Русский

Для любых a,b: ∂b ≤ ∂(a ∨ b) ∨ ∂(a ∧ b).

LaTeX

$$$ ∂ b \le ∂ (a \vee b) \vee ∂ (a \wedge b) $$$

Lean4

theorem boundary_le_boundary_sup_sup_boundary_inf_right : ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) :=
  by
  rw [sup_comm a, inf_comm]
  exact boundary_le_boundary_sup_sup_boundary_inf_left

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

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

Разделы

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

Аффилиация

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