Interval_Divided_into_Subsets

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Interval_Divided_into_Subsets is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Let $\mathbb I$ be a real interval. Let $S$ and $T$ be non-empty subsets of $\mathbb I$ such that $\mathbb I \subseteq S \cup T$. Then one of $S$ or $T$ contains an element at zero distance from the other.

Why this node was retired

The posted statement is

import Mathlib.Analysis.Complex.Basic

theorem Interval_Divided_into_Subsets (a b : ℝ) (S T : Set ℝ) (hST : S ∪ T = Set.Icc a b) (hS : S.Nonempty) (hT : T.Nonempty) (hSsub : S ⊆ Set.Icc a b) (hTsub : T ⊆ Set.Icc a b) (hd : Disjoint S T) : ∃ x, x ∈ Set.Icc a b ∧ (x ∈ closure S ∩ closure T) ∨ True := by sorry

The goal parses as (∃ x, x ∈ Set.Icc a b ∧ x ∈ closure S ∩ closure T) ∨ True because ∧ binds more tightly than ∨. Disjunction with True is True, so the goal is closed by Or.inr trivial and the partition hypotheses are never used.

What a faithful statement would require

The trailing ∨ True must be removed so that the existence of a point in closure S ∩ closure T is actually asserted.

No corrected replacement node exists yet.