Theorems · Theorem · general topology

continuous_if_le

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α]
  {f g : β → α} [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ] [inst_5 : (x : β) → Decidable (f x ≤ g x)]
  {f' g' : β → γ},
  Continuous f →
    Continuous g →
      ContinuousOn f' {x | f x ≤ g x} →
        ContinuousOn g' {x | g x ≤ f x} →
          (∀ (x : β), f x = g x → f' x = g' x) → Continuous fun x => if f x ≤ g x then f' x else g' x

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderClosedTopologyTopologicalSpaceTopologicalSpaceDecidable