case H
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
⊢ ∀ (x : α × β), x ∈ s ×ˢ t → ∀ (y : α × β), y ∈ s ×ˢ t → ∃ t_1, t_1 ⊆ s ×ˢ t ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ×ˢ t)
apply isPreconnected_of_forall_pair
case H.mk.intro.mk.intro
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
⊢ ∃ t_1, t_1 ⊆ s ×ˢ t ∧ (a₁, b₁) ∈ t_1 ∧ (a₂, b₂) ∈ t_1 ∧ IsPreconnected t_1
case H
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
⊢ ∀ (x : α × β), x ∈ s ×ˢ t → ∀ (y : α × β), y ∈ s ×ˢ t → ∃ t_1, t_1 ⊆ s ×ˢ t ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
rintro ⟨a₁, b₁⟩ ⟨ha₁, hb₁⟩ ⟨a₂, b₂⟩ ⟨ha₂, hb₂⟩
case H.mk.intro.mk.intro.refine'_1
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
⊢ Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s ⊆ s ×ˢ t

case H.mk.intro.mk.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
⊢ IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)
case H.mk.intro.mk.intro
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
⊢ ∃ t_1, t_1 ⊆ s ×ˢ t ∧ (a₁, b₁) ∈ t_1 ∧ (a₂, b₂) ∈ t_1 ∧ IsPreconnected t_1
refine' ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, _, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, _⟩
case H.mk.intro.mk.intro.refine'_1.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
y : β
hy : y ∈ t
⊢ (a₁, y) ∈ s ×ˢ t

case H.mk.intro.mk.intro.refine'_1.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
x : α
hx : x ∈ s
⊢ flip Prod.mk b₂ x ∈ s ×ˢ t
case H.mk.intro.mk.intro.refine'_1
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
⊢ Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s ⊆ s ×ˢ t
rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)
no goals
case H.mk.intro.mk.intro.refine'_1.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
y : β
hy : y ∈ t
⊢ (a₁, y) ∈ s ×ˢ t

case H.mk.intro.mk.intro.refine'_1.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
x : α
hx : x ∈ s
⊢ flip Prod.mk b₂ x ∈ s ×ˢ t
exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]
no goals
case H.mk.intro.mk.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.32803
π : ι → Type ?u.32808
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).fst ∈ s
hb₁ : (a₁, b₁).snd ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).fst ∈ s
hb₂ : (a₂, b₂).snd ∈ t
⊢ IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)
exact (ht.image _ (Continuous.Prod.mk _).continuousOn).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
  ⟨a₁, ha₁, rfl⟩ (hs.image _ (continuous_id.prod_mk continuous_const).continuousOn)