Mathlib Map

Theorems · Theorem · order theory

Coheyting.boundary_inf

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

Leibniz rule for the co-Heyting boundary.

Defined in
Mathlib.Order.Heyting.Boundary
Cited by
1 results in Mathlib
Foundations
Depth 12 from the axioms · uses propext
Assumes
CoheytingAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Coheyting.boundary_inf_le · cited by 1Coheyting.boundary_inf_leCoheytingAlgebra · cited by 96CoheytingAlgebraHNot.hnot · cited by 83HNot.hnotinf_assoc · cited by 53inf_associnf_sup_left · cited by 28inf_sup_leftCoheyting.boundary · cited by 24Coheyting.boundaryinf_right_comm · cited by 9inf_right_commhnot_inf_distrib · cited by 6hnot_inf_distribCoheyting.boundary_infCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.