case mp
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
⊢ IsCompact U ∧ IsOpen U → ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i

case mpr
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
⊢ (∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i) → IsCompact U ∧ IsOpen U
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
constructor
case mp.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
case mp
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
⊢ IsCompact U ∧ IsOpen U → ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
rintro ⟨h₁, h₂⟩
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f : β → Set α
e : U = ⋃ (i : β), f i
hf : ∀ (i : β), f i ∈ range b
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
case mp.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
obtain ⟨β, f, e, hf⟩ := hb.open_eq_iUnion h₂
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f : β → Set α
e : U = ⋃ (i : β), f i
f' : β → ι
hf' : ∀ (i : β), b (f' i) = f i
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f : β → Set α
e : U = ⋃ (i : β), f i
hf : ∀ (i : β), f i ∈ range b
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
choose f' hf' using hf
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f : β → Set α
e : U = ⋃ (i : β), f i
f' : β → ι
hf' : ∀ (i : β), b (f' i) = f i
this : b ∘ f' = f
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f : β → Set α
e : U = ⋃ (i : β), f i
f' : β → ι
hf' : ∀ (i : β), b (f' i) = f i
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
have : b ∘ f' = f := funext hf'
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f : β → Set α
e : U = ⋃ (i : β), f i
f' : β → ι
hf' : ∀ (i : β), b (f' i) = f i
this : b ∘ f' = f
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
subst this
case mp.intro.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
obtain ⟨t, ht⟩ :=
  h₁.elim_finite_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) (by rw [e])
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ U ≤ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i

case mp.intro.intro.intro.intro.intro.refine'_2
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ (⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i) ≤ U
case mp.intro.intro.intro.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i
refine' ⟨t.image f', Set.Finite.intro inferInstance, le_antisymm _ _⟩
no goals
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
⊢ U ⊆ ⋃ (i : β), (b ∘ f') i
rw [e]
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ (⋃ (i : β) (_ : i ∈ t), (b ∘ f') i) ⊆ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ U ≤ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i
refine' Set.Subset.trans ht _
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ ∀ (i : β), i ∈ t → (b ∘ f') i ⊆ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ (⋃ (i : β) (_ : i ∈ t), (b ∘ f') i) ⊆ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i
simp only [Set.iUnion_subset_iff]
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
i : β
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ ∀ (i : β), i ∈ t → (b ∘ f') i ⊆ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i
intro i hi
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
i : β
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ (x : { x // x ∈ Finset.image f' t }), b ↑x
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
i : β
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i
erw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]
no goals
case mp.intro.intro.intro.intro.intro.refine'_1
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
i : β
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ (x : { x // x ∈ Finset.image f' t }), b ↑x
exact Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, Finset.mem_image_of_mem _ hi⟩
case mp.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ ∀ (i : ι), i ∈ ↑(Finset.image f' t) → b i ⊆ U
case mp.intro.intro.intro.intro.intro.refine'_2
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ (⋃ (i : ι) (_ : i ∈ ↑(Finset.image f' t)), b i) ≤ U
apply Set.iUnion₂_subset
case mp.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
i : ι
hi : i ∈ ↑(Finset.image f' t)
⊢ b i ⊆ U
case mp.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
⊢ ∀ (i : ι), i ∈ ↑(Finset.image f' t) → b i ⊆ U
rintro i hi
case mp.intro.intro.intro.intro.intro.refine'_2.h.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
j : β
hi : f' j ∈ ↑(Finset.image f' t)
⊢ b (f' j) ⊆ U
case mp.intro.intro.intro.intro.intro.refine'_2.h
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
i : ι
hi : i ∈ ↑(Finset.image f' t)
⊢ b i ⊆ U
obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
case mp.intro.intro.intro.intro.intro.refine'_2.h.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
j : β
hi : f' j ∈ ↑(Finset.image f' t)
⊢ b (f' j) ⊆ ⋃ (i : β), (b ∘ f') i
case mp.intro.intro.intro.intro.intro.refine'_2.h.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
j : β
hi : f' j ∈ ↑(Finset.image f' t)
⊢ b (f' j) ⊆ U
rw [e]
no goals
case mp.intro.intro.intro.intro.intro.refine'_2.h.intro.intro
α : Type u
β✝ : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
s t✝ : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
h₁ : IsCompact U
h₂ : IsOpen U
β : Type u
f' : β → ι
e : U = ⋃ (i : β), (b ∘ f') i
hf' : ∀ (i : β), b (f' i) = (b ∘ f') i
t : Finset β
ht : U ⊆ ⋃ (i : β) (_ : i ∈ t), (b ∘ f') i
j : β
hi : f' j ∈ ↑(Finset.image f' t)
⊢ b (f' j) ⊆ ⋃ (i : β), (b ∘ f') i
exact Set.subset_iUnion (b ∘ f') j
case mpr.intro.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : Set.Finite s
⊢ IsCompact (⋃ (i : ι) (_ : i ∈ s), b i) ∧ IsOpen (⋃ (i : ι) (_ : i ∈ s), b i)
case mpr
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set α
⊢ (∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), b i) → IsCompact U ∧ IsOpen U
rintro ⟨s, hs, rfl⟩
case mpr.intro.intro.left
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : Set.Finite s
⊢ IsCompact (⋃ (i : ι) (_ : i ∈ s), b i)

case mpr.intro.intro.right
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : Set.Finite s
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), b i)
case mpr.intro.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : Set.Finite s
⊢ IsCompact (⋃ (i : ι) (_ : i ∈ s), b i) ∧ IsOpen (⋃ (i : ι) (_ : i ∈ s), b i)
constructor
no goals
case mpr.intro.intro.left
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : Set.Finite s
⊢ IsCompact (⋃ (i : ι) (_ : i ∈ s), b i)
exact hs.isCompact_biUnion fun i _ => hb' i
no goals
case mpr.intro.intro.right
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.42425
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
b : ι → Set α
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : Set.Finite s
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), b i)
exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)