α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.14103
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : γ → β
⊢ (⨅ (i : Set α) (_ : i ∈ f), comap m (g i)) = ⨅ (s : Set α) (_ : s ∈ f), (comap m ∘ g) s
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.14103
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : γ → β
⊢ comap m (Filter.lift f g) = Filter.lift f (comap m ∘ g)
simp only [Filter.lift, comap_iInf]
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.14103
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : γ → β
⊢ (⨅ (i : Set α) (_ : i ∈ f), comap m (g i)) = ⨅ (s : Set α) (_ : s ∈ f), (comap m ∘ g) s
rfl