mathlib
70a4f219 - refactor(measure_theory/measure/mutually_singular): use ⟂ PERPENDICULAR instead of ⊥ UP TACK (#18423)

Commit
2 years ago
refactor(measure_theory/measure/mutually_singular): use ⟂ PERPENDICULAR instead of ⊥ UP TACK (#18423) The previous notation for `measure_theory.measure.mutually_singular` was `⊥ₘ`. This changes it to `⟂ₘ`, which is semantically a better character. The same change is made for `measure_theory.vector_measure.mutually_singular`, from `⊥ᵥ` to `⟂ᵥ`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Perpendicular.20notation/near/327158463)
Author
Parents
Loading