α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.161619
β : Type ?u.161623
γ : Type ?u.161632
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
this : UniformSpace α
⊢ Sort ?u.161779
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.161619
β : Type ?u.161623
γ : Type ?u.161632
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
⊢ Sort ?u.161779
haveI := sInf uas
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.161619
β : Type ?u.161623
γ : Type ?u.161632
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.161779
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.161619
β : Type ?u.161623
γ : Type ?u.161632
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
this : UniformSpace α
⊢ Sort ?u.161779
haveI := sInf ubs
no goals
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.161619
β : Type ?u.161623
γ : Type ?u.161632
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.161779
exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
⊢ UniformContinuous fun p => f p.fst p.snd
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
⊢ UniformContinuous fun p => f p.fst p.snd
let _ : UniformSpace (α × β) := instUniformSpaceProd
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
⊢ UniformContinuous fun p => f p.fst p.snd
have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
hb : UniformContinuous id
h_unif_cont_id : UniformContinuous (Prod.map id id)
⊢ UniformContinuous fun p => f p.fst p.snd
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
have h_unif_cont_id := @UniformContinuous.prod_map _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb
no goals
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort ?u.161591
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
hb : UniformContinuous id
h_unif_cont_id : UniformContinuous (Prod.map id id)
⊢ UniformContinuous fun p => f p.fst p.snd
exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id