mathlib
dcedc047 - feat(order/symm_diff): Triangle inequality for the symmetric difference (#14847)

Commit

3 years ago

feat(order/symm_diff): Triangle inequality for the symmetric difference (#14847) Prove that `a ∆ c ≤ a ∆ b ⊔ b ∆ c`.

Author

YaelDillies

Parents