Theorems · Theorem · general topology

IsClosed.mem_of_ge_of_forall_exists_gt

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {a b : α}
  {s : Set α}, IsClosed (s ∩ Set.Icc a b) → a ∈ s → a ≤ b → (∀ x ∈ s ∩ Set.Ico a b, (s ∩ Set.Ioc x b).Nonempty) → b ∈ s

A "continuous induction principle" for a closed interval: if a set s meets [a, b] on a closed subset, contains a, and the set s ∩ [a, b) has no maximal point, then b ∈ s.

Defined in

Mathlib.Topology.Order.IntermediateValue

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceConditionallyCompleteLinearOrderOrderTopology