Theorems · Theorem · general topology

continuous_if

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {p : α → Prop}
  [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ frontier {x | p x}, f a = g a) →
    ContinuousOn f (closure {x | p x}) →
      ContinuousOn g (closure {x | ¬p x}) → Continuous fun a => if p a then f a else g a

Defined in

Mathlib.Topology.Piecewise

Cited by

3 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceDecidable