Commit 2023-02-12 08:45 70a4f219
View on Github →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