map_pi_map_coprodᵢ_le — Mathlib

English

A mapping inequality showing that map composed with coprodᵢ is less than coprodᵢ of mapped components.

Русский

Неравенство отображения, показывающее, что композиция map и coprodᵢ меньше coprodᵢ отображения компонент.

LaTeX

$$map_pi_map_coprodᵢ_le :$$

Lean4

theorem map_pi_map_coprodᵢ_le :
    map (fun k : ∀ i, α i => fun i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => map (m i) (f i) :=
  by
  simp only [le_def, mem_map, mem_coprodᵢ_iff]
  intro s h i
  obtain ⟨t, H, hH⟩ := h i
  exact ⟨{x : α i | m i x ∈ t}, H, fun x hx => hH hx⟩

Похожие утверждения