Coheyting.boundary_inf

theorem Coheyting.boundary_inf : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a b : α), Coheyting.boundary (a ⊓ b) = Coheyting.boundary a ⊓ b ⊔ a ⊓ Coheyting.boundary b

This theorem states the **Leibniz rule** for the boundary in a co-Heyting algebra. Given any co-Heyting algebra and two elements `a` and `b` in that algebra, the boundary of the infimum (greatest lower bound) of `a` and `b` is equal to the supremum (least upper bound) of the infimum of the boundary of `a` and `b`, and the infimum of `a` and the boundary of `b`. In mathematical terms, this can be written as $\partial(a \land b) = (\partial a \land b) \lor (a \land \partial b)$, where $\partial$ denotes the boundary operation, $\land$ denotes the infimum, and $\lor$ denotes the supremum.

More concisely: The boundary of the infimum of two elements in a co-Heyting algebra equals the supremum of the infimum of their boundaries and the infimum of each element with its boundary.