Alt connected set def in textbook

Stream: general

[Ender Doe]

So recently I have been trying to prove theorems from my real analysis textbook. One thing Ive noticed is that many real analysis books have an alternate definition of connectedness, then the standard one, which is in lean. Here is a great SO question explaining this https://math.stackexchange.com/questions/115190/connecting-two-definitions-of-connectedness?rq=1. Some of the theorems I wanted to prove following the logic in the book use this version of connectedness. I was not able to find a theorem for this in Math lib, so I proved it (good exercise).

theorem connected_iff_alt_connected {α : Type u} [topological_space  α] (E : set α) :
is_preconnected E ↔ ¬∃ (A B : set α), E = A ∪ B ∧ A ∩ closure B = ∅ ∧ closure A ∩ B = ∅ ∧ A.nonempty ∧ B.nonempty

I have two questions then,

1. Did I miss this lemma in mathlib?
2. If not would this be worth having in mathlib?

Thanks for your patience.

[Patrick Massot]

I'm pretty sure we don't have this lemma. I've never seen this definition of connectedness. Do you have any example of a proof where this is convenient?

[Ender Doe]

Follow up on this, I did a bit more research and it seems like some books may have this definition for pedagogical reasons. In Principles of Mathematical Analysis, they use it for proving that a connected set $E$ mapped by a continuous function $f$ implies $f(E)$ is connected (For metric spaces). This lecture on youtube uses this definition https://www.youtube.com/watch?v=dazO9UoKmyA&t=2912s (link has timestamp). I was using it for proving the
the following,

Let $I = [0, 1]$ be the closed unit interval. Suppose $f$ is a continuous mapping of $I$ into $I$. Prove that $f(x) = x$ for at least one $x \in I$.

I think perhaps this might make mores sense in a separate repository then, its rather interesting running into these issues trying to follow random theorems from textbooks.