English
A preconnected subset in an ordered space belongs to the union of canonical interval ranges.
Русский
Предсвязанный подмножество в упорядоченном пространстве принадлежит объединению канонических интервалов.
LaTeX
$$$IsPreconnected(s) \Rightarrow s \in \text{canonical-interval-union}$$$
Lean4
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `x ∈ [a, b)` such that `[a, x]` is included in `s`,
the set `s` includes some open neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`. -/
theorem Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s)
(h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t) : Icc a b ⊆ s :=
by
rcases lt_or_ge b a with hab | hab
· simp_all
set A := {t ∈ Icc a b | Icc a t ⊆ s}
have a_mem : a ∈ A := ⟨left_mem_Icc.mpr hab, by simp [ha]⟩
have bdd_A : BddAbove A := ⟨b, fun t ht ↦ ht.1.2⟩
set t₁ := sSup A
have t₁_mem : t₁ ∈ Icc a b := ⟨le_csSup bdd_A a_mem, csSup_le ⟨a, a_mem⟩ (fun t ht ↦ ht.1.2)⟩
obtain ⟨⟨t₁a, t₁b⟩, ht₁⟩ : t₁ ∈ A := by
refine ⟨t₁_mem, fun t ht ↦ ?_⟩
rcases ht.2.eq_or_lt with rfl | h
· have : closure A ⊆ s ∩ Icc a b :=
by
apply (closure_subset_iff hs).2 (fun t ht ↦ ⟨?_, ht.1⟩)
have : t ∈ Icc a t := ⟨ht.1.1, le_rfl⟩
exact ht.2 this
apply this.trans inter_subset_left
exact csSup_mem_closure ⟨a, a_mem⟩ bdd_A
· obtain ⟨c, cA, tc⟩ : ∃ c ∈ A, t < c := (lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h
apply cA.2
exact ⟨ht.1, tc.le⟩
suffices t₁ = b by simpa [this] using ht₁
apply eq_of_le_of_not_lt t₁b fun t₁b' ↦ ?_
obtain ⟨m, t₁m, H⟩ : ∃ m > t₁, Ioo t₁ m ⊆ s :=
(mem_nhdsGT_iff_exists_Ioo_subset' t₁b').mp (h t₁ ⟨t₁a, t₁b'⟩ (fun s hs ↦ ht₁ hs))
obtain ⟨t, hat, ht⟩ : ∃ t, t₁ < t ∧ t < min m b := exists_between (lt_min t₁m t₁b')
have : t ∈ A := by
refine ⟨⟨by order, ht.le.trans (min_le_right _ _)⟩, fun t' ht' ↦ ?_⟩
rcases le_or_gt t' t₁ with h't' | h't'
· exact ht₁ ⟨ht'.1, h't'⟩
· exact H ⟨h't', ht'.2.trans_lt <| ht.trans_le <| min_le_left ..⟩
have : t ≤ t₁ := le_csSup bdd_A this
order
