case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : f x ∈ u
y : α
hy : y ∈ s
hyv : f y ∈ v
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
⊢ IsPreirreducible (f '' s)
rintro u v hu hv ⟨_, ⟨⟨x, hx, rfl⟩, hxu⟩⟩ ⟨_, ⟨⟨y, hy, rfl⟩, hyv⟩⟩
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : f x ∈ u
y : α
hy : y ∈ s
hyv : f y ∈ v
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
rw [← mem_preimage] at hxu hyv
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (s ∩ u') → Set.Nonempty (s ∩ v') → Set.Nonempty (s ∩ (u' ∩ v'))
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
have := H u' v' hu' hv'
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (s ∩ v') → Set.Nonempty (s ∩ (u' ∩ v'))
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (s ∩ u') → Set.Nonempty (s ∩ v') → Set.Nonempty (s ∩ (u' ∩ v'))
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
rw [inter_comm s u', ← u'_eq] at this
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (s ∩ v') → Set.Nonempty (s ∩ (u' ∩ v'))
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
rw [inter_comm s v', ← v'_eq] at this
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
rcases this ⟨x, hxu, hx⟩ ⟨y, hyv, hy⟩ with ⟨z, hzs, hzu', hzv'⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ f z ∈ u

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ f z ∈ v
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ Set.Nonempty (f '' s ∩ (u ∩ v))
refine' ⟨f z, mem_image_of_mem f hzs, _, _⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ f z ∈ u

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ f z ∈ v
all_goals
  rw [← mem_preimage]
  apply mem_of_mem_inter_left
  show z ∈ _ ∩ s
  simp [*]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ z ∈ f ⁻¹' v
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ f z ∈ v
rw [← mem_preimage]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ z ∈ f ⁻¹' v ∩ ?intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.b

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.b
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ Set α
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ z ∈ f ⁻¹' v
apply mem_of_mem_inter_left
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ z ∈ f ⁻¹' v ∩ s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ z ∈ f ⁻¹' v ∩ ?intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.b

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.b
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ Set α
show z ∈ _ ∩ s
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β : Type v
ι : Type ?u.188216
π : ι → Type ?u.188221
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : IsPreirreducible s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen u
hv : IsOpen v
x : α
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : α
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set α
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : Set.Nonempty (f ⁻¹' u ∩ s) → Set.Nonempty (f ⁻¹' v ∩ s) → Set.Nonempty (s ∩ (u' ∩ v'))
z : α
hzs : z ∈ s
hzu' : z ∈ u'
hzv' : z ∈ v'
⊢ z ∈ f ⁻¹' v ∩ s
simp [*]