Theorems · Theorem · general topology

IsConnected.Icc_subset

∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {s : Set α},
  IsConnected s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.Icc a b ⊆ s

If a preconnected set contains endpoints of an interval, then it includes the whole interval.

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

LinearOrderTopologicalSpaceOrderClosedTopology