Theorem IsOpen.relComp

Modification history

2025-08-13 00:55
Mathlib/Topology/UniformSpace/Basic.lean
refactor: rename `Rel` to `SetRel`, restore the old `Rel` (#27447) …
Modified IsOpen.relCompView on Github →
2025-07-11 02:59
Mathlib/Topology/UniformSpace/Basic.lean
feat: the composition of open relations is open (#24173) …
Added IsOpen.relCompView on Github →