case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u v : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
constructor <;> intro h
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u v : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
intro u v hu hv hs huv
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → Set.Nonempty (s ∩ t) → Set.Nonempty (s ∩ t') → Set.Nonempty (s ∩ (t ∩ t'))
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
rw [isPreconnected_closed_iff] at h
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
⊢ s ⊆ u ∨ s ⊆ v
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → Set.Nonempty (s ∩ t) → Set.Nonempty (s ∩ t') → Set.Nonempty (s ∩ (t ∩ t'))
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
specialize h u v hu hv hs
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ s ∩ (u ∩ v) ≠ ∅
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
⊢ s ⊆ u ∨ s ⊆ v
contrapose! huv
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ s ∩ (u ∩ v) ≠ ∅
rw [← nonempty_iff_ne_empty]
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
huv : (∃ a, a ∈ s ∧ ¬a ∈ u) ∧ ∃ a, a ∈ s ∧ ¬a ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
simp [not_subset] at huv
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
x : α
hxs : x ∈ s
hxu : ¬x ∈ u
y : α
hys : y ∈ s
hyv : ¬y ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mp
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
huv : (∃ a, a ∈ s ∧ ¬a ∈ u) ∧ ∃ a, a ∈ s ∧ ¬a ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
x : α
hxs : x ∈ s
hxu : ¬x ∈ u
y : α
hys : y ∈ s
hyv : ¬y ∈ v
hxv : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
x : α
hxs : x ∈ s
hxu : ¬x ∈ u
y : α
hys : y ∈ s
hyv : ¬y ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
x : α
hxs : x ∈ s
hxu : ¬x ∈ u
y : α
hys : y ∈ s
hyv : ¬y ∈ v
hxv : x ∈ v
hyu : y ∈ u
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
x : α
hxs : x ∈ s
hxu : ¬x ∈ u
y : α
hys : y ∈ s
hyv : ¬y ∈ v
hxv : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
no goals
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
x : α
hxs : x ∈ s
hxu : ¬x ∈ u
y : α
hys : y ∈ s
hyv : ¬y ∈ v
hxv : x ∈ v
hyu : y ∈ u
⊢ Set.Nonempty (s ∩ (u ∩ v))
exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → Set.Nonempty (s ∩ t) → Set.Nonempty (s ∩ t') → Set.Nonempty (s ∩ (t ∩ t'))
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s
rw [isPreconnected_closed_iff]
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → Set.Nonempty (s ∩ t) → Set.Nonempty (s ∩ t') → Set.Nonempty (s ∩ (t ∩ t'))
intro u v hu hv hs hsu hsv
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
⊢ s ∩ (u ∩ v) ≠ ∅
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
⊢ Set.Nonempty (s ∩ (u ∩ v))
rw [nonempty_iff_ne_empty]
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : s ∩ (u ∩ v) = ∅
⊢ False
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
⊢ s ∩ (u ∩ v) ≠ ∅
intro H
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : s ∩ (u ∩ v) = ∅
h : s ⊆ u ∨ s ⊆ v
⊢ False
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : s ∩ (u ∩ v) = ∅
⊢ False
specialize h u v hu hv hs H
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
h : s ⊆ u ∨ s ⊆ v
H : ¬False
⊢ ¬s ∩ (u ∩ v) = ∅
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : s ∩ (u ∩ v) = ∅
h : s ⊆ u ∨ s ⊆ v
⊢ False
contrapose H
case mpr.a
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
h : s ⊆ u ∨ s ⊆ v
H : ¬False
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mpr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
h : s ⊆ u ∨ s ⊆ v
H : ¬False
⊢ ¬s ∩ (u ∩ v) = ∅
apply Nonempty.ne_empty
case mpr.a.inl
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : ¬False
h : s ⊆ u
⊢ Set.Nonempty (s ∩ (u ∩ v))

case mpr.a.inr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : ¬False
h : s ⊆ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mpr.a
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
h : s ⊆ u ∨ s ⊆ v
H : ¬False
⊢ Set.Nonempty (s ∩ (u ∩ v))
cases' h with h h
case mpr.a.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
H : ¬False
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mpr.a.inl
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : ¬False
h : s ⊆ u
⊢ Set.Nonempty (s ∩ (u ∩ v))
rcases hsv with ⟨x, hxs, hxv⟩
no goals
case mpr.a.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
H : ¬False
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩
case mpr.a.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsv : Set.Nonempty (s ∩ v)
H : ¬False
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ Set.Nonempty (s ∩ (u ∩ v))
case mpr.a.inr
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hsv : Set.Nonempty (s ∩ v)
H : ¬False
h : s ⊆ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
rcases hsu with ⟨x, hxs, hxu⟩
no goals
case mpr.a.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.102865
π : ι → Type ?u.102870
inst✝ : TopologicalSpace α
s t u✝ v✝ u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsv : Set.Nonempty (s ∩ v)
H : ¬False
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ Set.Nonempty (s ∩ (u ∩ v))
exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩