case a
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ G

case a
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ G ≤ map f (F ⊓ comap f G)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) = map f F ⊓ G
apply le_antisymm
no goals
case a
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ G
calc
  map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
  _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le
case a.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ U ∈ map f F ⊓ G
case a
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ G ≤ map f (F ⊓ comap f G)
rintro U ⟨V, V_in, W, ⟨Z, Z_in, hZ⟩, h⟩
case a.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z ⊆ U
case a.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ U ∈ map f F ⊓ G
apply mem_inf_of_inter (image_mem_map V_in) Z_in
no goals
case a.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z ⊆ U
calc
  f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
  _ ⊆ f '' (V ∩ W) := image_subset _ (inter_subset_inter_right _ ‹_›)
  _ = f '' (f ⁻¹' U) := by rw [h]
  _ ⊆ U := image_preimage_subset f U
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)
rw [image_inter_preimage]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.286447
ι : Sort x
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ W) = f '' (f ⁻¹' U)
rw [h]