case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro
α : Type u
β : Type v
ι : Type ?u.189901
π : ι → Type ?u.189906
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsPreirreducible s
u : Set α
hu : IsOpen u
v : Set α
hv : IsOpen v
x : α
hxs : x ∈ s
hxu : { val := x, property := hxs } ∈ val ⁻¹' u
y : α
hys : y ∈ s
hyv : { val := y, property := hys } ∈ val ⁻¹' v
⊢ Set.Nonempty (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v))
α : Type u
β : Type v
ι : Type ?u.189901
π : ι → Type ?u.189906
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsPreirreducible s
⊢ IsPreirreducible univ
rintro _ _ ⟨u, hu, rfl⟩ ⟨v, hv, rfl⟩ ⟨⟨x, hxs⟩, -, hxu⟩ ⟨⟨y, hys⟩, -, hyv⟩
case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.189901
π : ι → Type ?u.189906
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsPreirreducible s
u : Set α
hu : IsOpen u
v : Set α
hv : IsOpen v
x : α
hxs : x ∈ s
hxu : { val := x, property := hxs } ∈ val ⁻¹' u
y : α
hys : y ∈ s
hyv : { val := y, property := hys } ∈ val ⁻¹' v
z : α
hzs : z ∈ s
hzu : z ∈ u
hzv : z ∈ v
⊢ Set.Nonempty (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v))
case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro
α : Type u
β : Type v
ι : Type ?u.189901
π : ι → Type ?u.189906
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsPreirreducible s
u : Set α
hu : IsOpen u
v : Set α
hv : IsOpen v
x : α
hxs : x ∈ s
hxu : { val := x, property := hxs } ∈ val ⁻¹' u
y : α
hys : y ∈ s
hyv : { val := y, property := hys } ∈ val ⁻¹' v
⊢ Set.Nonempty (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v))
rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨z, hzs, ⟨hzu, hzv⟩⟩
no goals
case intro.intro.intro.intro.intro.mk.intro.intro.mk.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.189901
π : ι → Type ?u.189906
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : IsPreirreducible s
u : Set α
hu : IsOpen u
v : Set α
hv : IsOpen v
x : α
hxs : x ∈ s
hxu : { val := x, property := hxs } ∈ val ⁻¹' u
y : α
hys : y ∈ s
hyv : { val := y, property := hys } ∈ val ⁻¹' v
z : α
hzs : z ∈ s
hzu : z ∈ u
hzv : z ∈ v
⊢ Set.Nonempty (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v))
exact ⟨⟨z, hzs⟩, ⟨Set.mem_univ _, ⟨hzu, hzv⟩⟩⟩