Mathlib Map

Theorems · Theorem · order theory

sup_sdiff

∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a ⊔ b) \ c = a \ c ⊔ b \ c
Defined in
Mathlib.Order.Heyting.Basic
Cited by
8 results in Mathlib
Foundations
Depth 10 from the axioms · uses propext
Assumes
GeneralizedCoheytingAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.union_sdiff_distrib · cited by 11Set.union_sdiff_distribsymmDiff_eq_sup_sdiff_inf · cited by 8symmDiff_eq_sup_sdiff_infsup_sdiff_right_self · cited by 6sup_sdiff_right_selfSimpleGraph.deleteEdges_sup · cited by 3SimpleGraph.deleteEdges_s…Finset.union_sdiff_distrib · cited by 2Finset.union_sdiff_distribsymmDiff_sdiff_left · cited by 2symmDiff_sdiff_leftUV.compress_sdiff_sdiff · cited by 1UV.compress_sdiff_sdiffFinset.sup_sdiff_right · cited by 1Finset.sup_sdiff_rightGeneralizedCoheytingAlgebra · cited by 95GeneralizedCoheytingAlgeb…sup_sdiff_distrib · cited by 5sup_sdiff_distribsup_sdiffCITED BYCITES

Cites2

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

Cited by8

Results whose statement or proof uses this declaration.