α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.map f f) atTop
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
⊢ Tendsto (Prod.map f f) atTop (𝓤 α)
intro s hs
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ a, ∀ (b : β × β), b ≥ a → b ∈ Prod.map f f ⁻¹' s
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.map f f) atTop
rw [mem_map, mem_atTop_sets]
case intro
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
⊢ ∃ a, ∀ (b : β × β), b ≥ a → b ∈ Prod.map f f ⁻¹' s
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ a, ∀ (b : β × β), b ≥ a → b ∈ Prod.map f f ⁻¹' s
cases' hU s hs with N hN
case intro
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
mn : β × β
hmn : mn ≥ (N, N)
⊢ mn ∈ Prod.map f f ⁻¹' s
case intro
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
⊢ ∃ a, ∀ (b : β × β), b ≥ a → b ∈ Prod.map f f ⁻¹' s
refine' ⟨(N, N), fun mn hmn => _⟩
case intro.mk
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
m n : β
hmn : (m, n) ≥ (N, N)
⊢ (m, n) ∈ Prod.map f f ⁻¹' s
case intro
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
mn : β × β
hmn : mn ≥ (N, N)
⊢ mn ∈ Prod.map f f ⁻¹' s
cases' mn with m n
no goals
case intro.mk
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → Set (α × α)
hU : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
m n : β
hmn : (m, n) ≥ (N, N)
⊢ (m, n) ∈ Prod.map f f ⁻¹' s
exact hN (hf hmn.1 hmn.2)