English
If Set.preimage of u under the Subtype.val is clopen and u is contained in v, then u equals the union over x∈u of connectedComponentIn v x.
Русский
Если предобраз через Subtype.val клино и u ⊆ v, то u равно объединению по x∈u connectedComponentIn v x.
LaTeX
$$$IsClopen(Set.preimage(Subtype.val, u)) \land (u \subseteq v) \Rightarrow u = \bigcup_{x\in u} connectedComponentIn v x$$$
Lean4
/-- If `u v : Set X` and `u ⊆ v` is clopen in `v`, then `u` is the union of the connected
components of `v` in `X` which intersect `u`. -/
theorem biUnion_connectedComponentIn {X : Type*} [TopologicalSpace X] {u v : Set X} (hu : IsClopen (v ↓∩ u))
(huv₁ : u ⊆ v) : u = ⋃ x ∈ u, connectedComponentIn v x :=
by
have := congr(((↑) : Set v → Set X) $(hu.biUnion_connectedComponent_eq.symm))
simp only [Subtype.image_preimage_coe, mem_preimage, iUnion_coe_set, image_val_iUnion,
inter_eq_right.mpr huv₁] at this
nth_rw 1 [this]
congr! 2 with x hx
simp only [← connectedComponentIn_eq_image]
exact
le_antisymm (iUnion_subset fun _ ↦ le_rfl) <| iUnion_subset fun hx ↦ subset_iUnion₂_of_subset (huv₁ hx) hx le_rfl
