boundary_inf — Mathlib

English

Let a,b ∈ α. The boundary operation satisfies a Leibniz-type rule with respect to inf and sup: ∂(a ∧ b) = ∂a ∧ b ⊔ a ∧ ∂b.

Русский

Пусть a,b ∈ α. Граница удовлетворяет правилу Лейбница относительно операций meet и join: ∂(a ∧ b) = ∂a ∧ b ∨ a ∧ ∂b.

LaTeX

$$$ \partial (a \wedge b) = (\partial a) \wedge b \vee a \wedge (\partial b) $$$

Lean4

/-- **Leibniz rule** for the co-Heyting boundary. -/
theorem boundary_inf (a b : α) : ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b :=
  by
  unfold boundary
  rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]

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