α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (f ⁻¹' s ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
hsf : s ⊆ range f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
⊢ Set.Nonempty (f ⁻¹' s ∩ (u ∩ v))
replace hsf : f '' (f ⁻¹' s) = s := image_preimage_eq_of_subset hsf
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (s ∩ (f '' u ∩ f '' v))

case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ Set.Nonempty (f ⁻¹' s ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (f ⁻¹' s ∩ (u ∩ v))
obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty
case refine_1
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ s ⊆ f '' u ∪ f '' v

case refine_2
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (s ∩ f '' u)

case refine_3
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (s ∩ f '' v)
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (s ∩ (f '' u ∩ f '' v))
refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
no goals
case refine_1
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ s ⊆ f '' u ∪ f '' v
simpa only [hsf, image_union] using image_subset f hsuv
no goals
case refine_2
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (s ∩ f '' u)
simpa only [image_preimage_inter] using hsu.image f
no goals
case refine_3
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
⊢ Set.Nonempty (s ∩ f '' v)
simpa only [image_preimage_inter] using hsv.image f
no goals
case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.25326
π : ι → Type ?u.25331
inst✝¹ : TopologicalSpace α
s✝ t u✝ v✝ : Set α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen u
hv : IsOpen v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : Set.Nonempty (f ⁻¹' s ∩ u)
hsv : Set.Nonempty (f ⁻¹' s ∩ v)
hsf : f '' (f ⁻¹' s) = s
a : α
hau : a ∈ u
has : f a ∈ s
hav : f a ∈ f '' v
⊢ Set.Nonempty (f ⁻¹' s ∩ (u ∩ v))
exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩