case intro.intro.intro.intro
α : Type u_1
α' : Type ?u.552
β : Type u_2
β' : Type ?u.558
γ : Type ?u.561
E : Type ?u.564
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : (⋃ (n : ℕ), s n) = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ IsCountablySpanning (image2 (fun x x_1 => x ×ˢ x_1) C D)
α : Type u_1
α' : Type ?u.552
β : Type u_2
β' : Type ?u.558
γ : Type ?u.561
E : Type ?u.564
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ IsCountablySpanning (image2 (fun x x_1 => x ×ˢ x_1) C D)
rcases hC, hD with ⟨⟨s, h1s, h2s⟩, t, h1t, h2t⟩
case intro.intro.intro.intro
α : Type u_1
α' : Type ?u.552
β : Type u_2
β' : Type ?u.558
γ : Type ?u.561
E : Type ?u.564
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : (⋃ (n : ℕ), s n) = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ (⋃ (n : ℕ), (fun n => s (Nat.unpair n).fst ×ˢ t (Nat.unpair n).snd) n) = univ
case intro.intro.intro.intro
α : Type u_1
α' : Type ?u.552
β : Type u_2
β' : Type ?u.558
γ : Type ?u.561
E : Type ?u.564
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : (⋃ (n : ℕ), s n) = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ IsCountablySpanning (image2 (fun x x_1 => x ×ˢ x_1) C D)
refine' ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), _⟩
no goals
case intro.intro.intro.intro
α : Type u_1
α' : Type ?u.552
β : Type u_2
β' : Type ?u.558
γ : Type ?u.561
E : Type ?u.564
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : (⋃ (n : ℕ), s n) = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ (⋃ (n : ℕ), (fun n => s (Nat.unpair n).fst ×ˢ t (Nat.unpair n).snd) n) = univ
rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]