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' →
      Continuous f →
        Continuous g → (∀ (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

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderClosedTopologyTopologicalSpaceTopologicalSpaceDecidable