α : Type u_2
β : Type ?u.74859
γ : Type u_1
ι : Type ?u.74865
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ (⨅ (i : Bool), uniformSpace α γ 𝔖) = ⨅ (b : Bool), bif b then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
α : Type u_2
β : Type ?u.74859
γ : Type u_1
ι : Type ?u.74865
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ uniformSpace α γ 𝔖
rw [inf_eq_iInf, inf_eq_iInf, UniformOnFun.iInf_eq]
α : Type u_2
β : Type ?u.74859
γ : Type u_1
ι : Type ?u.74865
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
α : Type u_2
β : Type ?u.74859
γ : Type u_1
ι : Type ?u.74865
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ (⨅ (i : Bool), uniformSpace α γ 𝔖) = ⨅ (b : Bool), bif b then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
refine' iInf_congr fun i => _
no goals
α : Type u_2
β : Type ?u.74859
γ : Type u_1
ι : Type ?u.74865
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
cases i <;> rfl