Commit 2024-11-19 11:04 1212c0ad

View on Github →

chore: some renames iff_open -> iff_isOpen (#19209) Our naming convention prefers isOpen. See the individual commit messages for details.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/Topology/Algebra/UniformGroup/Defs.lean

added theorem UniformGroup.uniformContinuous_iff_isOpen_ker

deleted theorem UniformGroup.uniformContinuous_iff_open_ker

Modified Mathlib/Topology/Connected/LocallyConnected.lean

added theorem locallyConnectedSpace_iff_hasBasis_isOpen_isConnected

deleted theorem locallyConnectedSpace_iff_open_connected_basis

deleted theorem locallyConnectedSpace_iff_open_connected_subsets

added theorem locallyConnectedSpace_iff_subsets_isOpen_isConnected

Modified Mathlib/Topology/Defs/Filter.lean

Modified Mathlib/Topology/Inseparable.lean

deleted theorem inseparable_iff_forall_closed

added theorem inseparable_iff_forall_isClosed

added theorem inseparable_iff_forall_isOpen

deleted theorem inseparable_iff_forall_open

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/Sets/Opens.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem isOpen_iff_isOpen_ball_subset

deleted theorem isOpen_iff_open_ball_subset