case a
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
⊢ pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)
ext t
case a
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ sᶜ ∪ f ⁻¹' t ∈ l ↔ {x | ¬x ∈ s ∨ x ∈ f ⁻¹' t} ∈ l
case a
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
simp only [PFun.core_res, mem_pmap, mem_map, mem_inf_principal, imp_iff_not_or]
no goals
case a
α : Type u
β : Type v
γ : Type w
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ sᶜ ∪ f ⁻¹' t ∈ l ↔ {x | ¬x ∈ s ∨ x ∈ f ⁻¹' t} ∈ l
rfl