English
The map of a coprod of two filters under Prod.map is contained in the coprod of the maps.
Русский
Образ отображения копродукта двух фильтров через Prod.map содержится в копродукт отображений.
LaTeX
$$$ \mathrm{map} (\mathrm{Prod.map} \ m_1 m_2) (f_1 \coprod f_2) \le (\mathrm{map} m_1 f_1) \ coprod (\mathrm{map} m_2 f_2). $$$
Lean4
theorem map_prodMap_coprod_le.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁}
{f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂) :=
by
intro s
simp only [mem_map, mem_coprod_iff]
rintro ⟨⟨u₁, hu₁, h₁⟩, u₂, hu₂, h₂⟩
refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩ <;> convert hx
