α : Type u
β : Type v
γ : Type w
δ : Type ?u.277101
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ ∅ ∈ map m f → ∅ ∈ f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.277101
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ map m f = ⊥ → f = ⊥
rw [← empty_mem_iff_bot, ← empty_mem_iff_bot]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.277101
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ ∅ ∈ map m f → ∅ ∈ f
exact id
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.277101
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
h : f = ⊥
⊢ map m f = ⊥
simp only [h, map_bot]