case a
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ S ∈ Filter.coprod (cocompact α) (cocompact β) ↔ S ∈ cocompact (α × β)
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ Filter.coprod (cocompact α) (cocompact β) = cocompact (α × β)
ext S
case a
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ ((∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧
      ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S) ↔
    ∃ t, IsCompact t ∧ tᶜ ⊆ S
case a
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ S ∈ Filter.coprod (cocompact α) (cocompact β) ↔ S ∈ cocompact (α × β)
simp only [mem_coprod_iff, exists_prop, mem_comap, Filter.mem_cocompact]
case a.mp
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ ((∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧
      ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S) →
    ∃ t, IsCompact t ∧ tᶜ ⊆ S

case a.mpr
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ S) →
    (∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧
      ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S
case a
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ ((∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧
      ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S) ↔
    ∃ t, IsCompact t ∧ tᶜ ⊆ S
constructor
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : tᶜ ⊆ A
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : t'ᶜ ⊆ B
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ S
case a.mp
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ ((∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧
      ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S) →
    ∃ t, IsCompact t ∧ tᶜ ⊆ S
rintro ⟨⟨A, ⟨t, ht, hAt⟩, hAS⟩, B, ⟨t', ht', hBt'⟩, hBS⟩
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : tᶜ ⊆ A
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : t'ᶜ ⊆ B
⊢ (t ×ˢ t')ᶜ ⊆ S
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : tᶜ ⊆ A
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : t'ᶜ ⊆ B
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ S
refine' ⟨t ×ˢ t', ht.prod ht', _⟩
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : tᶜ ⊆ A
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : t'ᶜ ⊆ B
⊢ (t ×ˢ t')ᶜ ⊆ Prod.fst ⁻¹' A ∪ Prod.snd ⁻¹' B
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : tᶜ ⊆ A
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : t'ᶜ ⊆ B
⊢ (t ×ˢ t')ᶜ ⊆ S
refine' Subset.trans _ (union_subset hAS hBS)
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : Aᶜ ⊆ t
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : Bᶜ ⊆ t'
⊢ (Prod.fst ⁻¹' A ∪ Prod.snd ⁻¹' B)ᶜ ⊆ t ×ˢ t'
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : tᶜ ⊆ A
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : t'ᶜ ⊆ B
⊢ (t ×ˢ t')ᶜ ⊆ Prod.fst ⁻¹' A ∪ Prod.snd ⁻¹' B
rw [compl_subset_comm] at hAt hBt'⊢
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : Aᶜ ⊆ t
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : Bᶜ ⊆ t'
x : α × β
⊢ x ∈ (Prod.fst ⁻¹' A ∪ Prod.snd ⁻¹' B)ᶜ → x ∈ Aᶜ ×ˢ Bᶜ
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : Aᶜ ⊆ t
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : Bᶜ ⊆ t'
⊢ (Prod.fst ⁻¹' A ∪ Prod.snd ⁻¹' B)ᶜ ⊆ t ×ˢ t'
refine' Subset.trans (fun x => _) (Set.prod_mono hAt hBt')
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : Aᶜ ⊆ t
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : Bᶜ ⊆ t'
x : α × β
⊢ ¬x.fst ∈ A ∧ ¬x.snd ∈ B → ¬x.fst ∈ A ∧ ¬x.snd ∈ B
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : Aᶜ ⊆ t
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : Bᶜ ⊆ t'
x : α × β
⊢ x ∈ (Prod.fst ⁻¹' A ∪ Prod.snd ⁻¹' B)ᶜ → x ∈ Aᶜ ×ˢ Bᶜ
simp only [compl_union, mem_inter_iff, mem_prod, mem_preimage, mem_compl_iff]
no goals
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S : Set (α × β)
A : Set α
hAS : Prod.fst ⁻¹' A ⊆ S
t : Set α
ht : IsCompact t
hAt : Aᶜ ⊆ t
B : Set β
hBS : Prod.snd ⁻¹' B ⊆ S
t' : Set β
ht' : IsCompact t'
hBt' : Bᶜ ⊆ t'
x : α × β
⊢ ¬x.fst ∈ A ∧ ¬x.snd ∈ B → ¬x.fst ∈ A ∧ ¬x.snd ∈ B
tauto
case a.mpr.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ (∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧ ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S
case a.mpr
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (α × β)
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ S) →
    (∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧
      ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S
rintro ⟨t, ht, htS⟩
case a.mpr.intro.intro.refine'_1
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ ∃ t_1, IsCompact t_1 ∧ t_1ᶜ ⊆ (Prod.fst '' t)ᶜ

case a.mpr.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ Prod.fst ⁻¹' (Prod.fst '' t)ᶜ ⊆ S

case a.mpr.intro.intro.refine'_3
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ ∃ t_1, IsCompact t_1 ∧ t_1ᶜ ⊆ (Prod.snd '' t)ᶜ

case a.mpr.intro.intro.refine'_4
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ Prod.snd ⁻¹' (Prod.snd '' t)ᶜ ⊆ S
case a.mpr.intro.intro
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ (∃ t₁, (∃ t, IsCompact t ∧ tᶜ ⊆ t₁) ∧ Prod.fst ⁻¹' t₁ ⊆ S) ∧ ∃ t₂, (∃ t, IsCompact t ∧ tᶜ ⊆ t₂) ∧ Prod.snd ⁻¹' t₂ ⊆ S
refine' ⟨⟨(Prod.fst '' t)ᶜ, _, _⟩, ⟨(Prod.snd '' t)ᶜ, _, _⟩⟩
no goals
case a.mpr.intro.intro.refine'_1
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ ∃ t_1, IsCompact t_1 ∧ t_1ᶜ ⊆ (Prod.fst '' t)ᶜ
exact ⟨Prod.fst '' t, ht.image continuous_fst, Subset.rfl⟩
case a.mpr.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ (Prod.fst ⁻¹' (Prod.fst '' t))ᶜ ⊆ S
case a.mpr.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ Prod.fst ⁻¹' (Prod.fst '' t)ᶜ ⊆ S
rw [preimage_compl]
case a.mpr.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : Sᶜ ⊆ t
⊢ Sᶜ ⊆ Prod.fst ⁻¹' (Prod.fst '' t)
case a.mpr.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ (Prod.fst ⁻¹' (Prod.fst '' t))ᶜ ⊆ S
rw [compl_subset_comm] at htS⊢
no goals
case a.mpr.intro.intro.refine'_2
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : Sᶜ ⊆ t
⊢ Sᶜ ⊆ Prod.fst ⁻¹' (Prod.fst '' t)
exact htS.trans (subset_preimage_image Prod.fst _)
no goals
case a.mpr.intro.intro.refine'_3
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ ∃ t_1, IsCompact t_1 ∧ t_1ᶜ ⊆ (Prod.snd '' t)ᶜ
exact ⟨Prod.snd '' t, ht.image continuous_snd, Subset.rfl⟩
case a.mpr.intro.intro.refine'_4
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ (Prod.snd ⁻¹' (Prod.snd '' t))ᶜ ⊆ S
case a.mpr.intro.intro.refine'_4
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ Prod.snd ⁻¹' (Prod.snd '' t)ᶜ ⊆ S
rw [preimage_compl]
case a.mpr.intro.intro.refine'_4
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : Sᶜ ⊆ t
⊢ Sᶜ ⊆ Prod.snd ⁻¹' (Prod.snd '' t)
case a.mpr.intro.intro.refine'_4
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : tᶜ ⊆ S
⊢ (Prod.snd ⁻¹' (Prod.snd '' t))ᶜ ⊆ S
rw [compl_subset_comm] at htS⊢
no goals
case a.mpr.intro.intro.refine'_4
α : Type u
β : Type v
ι : Type ?u.99857
π : ι → Type ?u.99862
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
S t : Set (α × β)
ht : IsCompact t
htS : Sᶜ ⊆ t
⊢ Sᶜ ⊆ Prod.snd ⁻¹' (Prod.snd '' t)
exact htS.trans (subset_preimage_image Prod.snd _)