Theorems · Theorem · general topology

IsClosed.mem_of_ge_of_forall_exists_lt

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

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

Defined in

Mathlib.Topology.Order.IntermediateValue

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceConditionallyCompleteLinearOrderOrderTopology