Theorems · Theorem · general topology

Continuous.if_ge

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

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderClosedTopologyTopologicalSpaceTopologicalSpaceDecidable