α : Type u
β : Type v
γ : Type w
δ : Type ?u.281757
ι : Sort x
f g : Filter α
m : α → β
h : Injective m
⊢ map m f ⊓ map m g ≤ map m (f ⊓ g)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.281757
ι : Sort x
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g
refine' map_inf_le.antisymm _
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.281757
ι : Sort x
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ t ∈ map m f ⊓ map m g
α : Type u
β : Type v
γ : Type w
δ : Type ?u.281757
ι : Sort x
f g : Filter α
m : α → β
h : Injective m
⊢ map m f ⊓ map m g ≤ map m (f ⊓ g)
rintro t ⟨s₁, hs₁, s₂, hs₂, ht : m ⁻¹' t = s₁ ∩ s₂⟩
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.281757
ι : Sort x
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.281757
ι : Sort x
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ t ∈ map m f ⊓ map m g
refine' mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) _
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.281757
ι : Sort x
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t
rw [← image_inter h, image_subset_iff, ht]