Commit 2024-02-15 06:24 c9a8b43e

View on Github →

feat(Topology/Constructions): add continuous_bool_rng (#10513) Provide continuity criteria for functions X → Bool and, more generally, X → Y, where Y has discrete topology.

Estimated changes

Modified Mathlib/Data/Bool/Basic.lean

added theorem Bool.exists_bool'

added theorem Bool.forall_bool'

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/Constructions.lean

added theorem continuous_bool_rng

Modified Mathlib/Topology/Order.lean

added theorem continuous_discrete_rng