Theorems · Theorem · general topology

IsClosed.isClosed_le

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f g : β → α} {s : Set β},
  IsClosed s → ContinuousOn f s → ContinuousOn g s → IsClosed {x | x ∈ s ∧ f x ≤ g x}

If s is a closed set and two functions f and g are continuous on s, then the set {x ∈ s | f x ≤ g x} is a closed set.

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorderOrderClosedTopologyTopologicalSpace