English
If m is injective, then map m preserves binary infimum exactly: map m (f ⊓ g) = map m f ⊓ map m g.
Русский
Если m инъективно, то отображение сохраняет точный бинарный inf: map m (f ⊓ g) = map m f ⊓ map m g.
LaTeX
$$map_inf {f g : Filter α} {m : α → β} (h : Injective m) : map m (f ⊓ g) = map m f ⊓ map m g$$
Lean4
theorem map_inf {f g : Filter α} {m : α → β} (h : Injective m) : map m (f ⊓ g) = map m f ⊓ map m g :=
by
refine map_inf_le.antisymm ?_
rintro t ⟨s₁, hs₁, s₂, hs₂, ht : m ⁻¹' t = s₁ ∩ s₂⟩
refine mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_
rw [← image_inter h, image_subset_iff, ht]
