English
For any MulHomClass m : F α β and filters f,g on β, the comap operation satisfies f.comap m * g.comap m ≤ (f * g).comap m.
Русский
Для любого m: F α β из класса MulHom, и фильтров f,g на β, операция comap удовлетворяет неравенству f.comap m * g.comap m ≤ (f * g).comap m.
LaTeX
$$$\forall m:\, F,\ f,g \in \mathrm{Filter}(\beta),\ f.{\mathrm comap}(m) * g.{\mathrm comap}(m) \le (f * g).{\mathrm comap}(m).$$$
Lean4
@[to_additive]
theorem comap_mul_comap_le [MulHomClass F α β] (m : F) {f g : Filter β} : f.comap m * g.comap m ≤ (f * g).comap m :=
fun _ ⟨_, ⟨t₁, ht₁, t₂, ht₂, t₁t₂⟩, mt⟩ =>
⟨m ⁻¹' t₁, ⟨t₁, ht₁, Subset.rfl⟩, m ⁻¹' t₂, ⟨t₂, ht₂, Subset.rfl⟩,
(preimage_mul_preimage_subset _).trans <| (preimage_mono t₁t₂).trans mt⟩
