case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Finset α
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hfin : Set.Finite s
hne : Set.Nonempty s
ho : IsOpen s
⊢ ∃ x, x ∈ s ∧ IsOpen {x}
lift s to Finset α using hfin
case intro.a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Finset α
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
induction' s using Finset.strongInductionOn with s ihs
case intro.a.inl.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
t : Finset α
hts : t ⊂ s
htne : Finset.Nonempty t
hto : IsOpen ↑t
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}

case intro.a.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
case intro.a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set α)) with (⟨t, hts, htne, hto⟩ | ht)
case intro.a.inl.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
t : Finset α
hts : t ⊂ s
htne : Finset.Nonempty t
hto : IsOpen ↑t
x : α
hxt : x ∈ ↑t
hxo : IsOpen {x}
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
case intro.a.inl.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
t : Finset α
hts : t ⊂ s
htne : Finset.Nonempty t
hto : IsOpen ↑t
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩
no goals
case intro.a.inl.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
t : Finset α
hts : t ⊂ s
htne : Finset.Nonempty t
hto : IsOpen ↑t
x : α
hxt : x ∈ ↑t
hxo : IsOpen {x}
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
exact ⟨x, hts.1 hxt, hxo⟩
case intro.a.inr.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
x : α
hx : ↑s = {x}
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
⊢ ∃ x, ↑s = {x}
case intro.a.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
rsuffices ⟨x, hx⟩ : ∃ x, s.toSet = {x}
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
⊢ ∀ (t : Set α), t ⊆ ↑s → Set.Nonempty t → IsOpen t → t = ↑s
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
⊢ ∃ x, ↑s = {x}
refine minimal_nonempty_open_eq_singleton ho hne ?_
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
t : Set α
hts : t ⊆ ↑s
htne : Set.Nonempty t
hto : IsOpen t
hts' : ¬t = ↑s
⊢ ∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
⊢ ∀ (t : Set α), t ⊆ ↑s → Set.Nonempty t → IsOpen t → t = ↑s
refine' fun t hts htne hto => of_not_not fun hts' => ht _
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
t : Finset α
hts : ↑t ⊆ ↑s
htne : Set.Nonempty ↑t
hto : IsOpen ↑t
hts' : ¬↑t = ↑s
⊢ ∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
t : Set α
hts : t ⊆ ↑s
htne : Set.Nonempty t
hto : IsOpen t
hts' : ¬t = ↑s
⊢ ∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
lift t to Finset α using s.finite_toSet.subset hts
no goals
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
t : Finset α
hts : ↑t ⊆ ↑s
htne : Set.Nonempty ↑t
hto : IsOpen ↑t
hts' : ¬↑t = ↑s
⊢ ∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩
no goals
case intro.a.inr.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s✝ : Finset α
hne✝ : Set.Nonempty ↑s✝
ho✝ : IsOpen ↑s✝
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → Set.Nonempty ↑t → IsOpen ↑t → ∃ x, x ∈ ↑t ∧ IsOpen {x}
hne : Set.Nonempty ↑s
ho : IsOpen ↑s
ht : ¬∃ t, t ⊂ s ∧ Finset.Nonempty t ∧ IsOpen ↑t
x : α
hx : ↑s = {x}
⊢ ∃ x, x ∈ ↑s ∧ IsOpen {x}
exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩