ι : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) ↔
    ∀ {ι : Type u_1} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ CompleteLattice.IsCompactElement s ↔ IsCompact ↑s
rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff]
case refine'_1
ι : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) →
    ∀ {ι : Type u_1} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i

case refine'_2
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ t, s ≤ Finset.sup t U
ι : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) ↔
    ∀ {ι : Type u_1} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
refine' ⟨_, fun H ι U hU => _⟩
case refine'_1
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
case refine'_1
ι : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) →
    ∀ {ι : Type u_1} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
introv H hU hU'
case refine'_1.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
case refine'_1
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
case refine'_1.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ↑(Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
case refine'_1.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
refine' ⟨t, Set.Subset.trans ht _⟩
case refine'_1.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ (⨆ (a : ι) (_ : a ∈ t), (SetLike.coe ∘ fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) a) ⊆
    ⋃ (i : ι) (_ : i ∈ t), U i
case refine'_1.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ↑(Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
rw [coe_finset_sup, Finset.sup_eq_iSup]
no goals
case refine'_1.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ (⨆ (a : ι) (_ : a ∈ t), (SetLike.coe ∘ fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) a) ⊆
    ⋃ (i : ι) (_ : i ∈ t), U i
rfl
no goals
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_1) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
⊢ s ≤ ⨆ (i : ι), { carrier := U i, is_open' := (_ : IsOpen (U i)) }
simpa
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∃ t, s ≤ Finset.sup t U
case refine'_2
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ t, s ≤ Finset.sup t U
obtain ⟨t, ht⟩ :=
  H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ (⋃ (i : ι) (_ : i ∈ t), ↑(U i)) ⊆ ↑(Finset.sup t U)
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∃ t, s ≤ Finset.sup t U
refine' ⟨t, Set.Subset.trans ht _⟩
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → ↑(U i) ⊆ ↑(Finset.sup t U)
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ (⋃ (i : ι) (_ : i ∈ t), ↑(U i)) ⊆ ↑(Finset.sup t U)
simp only [Set.iUnion_subset_iff]
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → U i ≤ Finset.sup t U
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → ↑(U i) ⊆ ↑(Finset.sup t U)
show ∀ i ∈ t, U i ≤ t.sup U
no goals
case refine'_2.intro
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → U i ≤ Finset.sup t U
exact fun i => Finset.le_sup
no goals
ι✝ : Type ?u.43879
α : Type u_1
β : Type ?u.43885
γ : Type ?u.43888
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → (↑s ⊆ ⋃ (i : ι), U i) → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_1
U : ι → Opens α
hU : s ≤ iSup U
⊢ ↑s ⊆ ⋃ (i : ι), (fun i => ↑(U i)) i
simpa using show (s : Set α) ⊆ ↑(iSup U) from hU