English
The left-distributive inequality direction holds in one way but not the other due to cross terms; given a distributive law, we have map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h).
Русский
Левая распределительная неравенство имеет направление, но другое направление может не выполняться из-за перекрестных членов; если выполнено тождество распределения, имеем неравенство: map₂ m f (map₂ n g h) ≤ …
LaTeX
$$$\mathrm{map}_2 m f (\mathrm{map}_2 n g h) \le \mathrm{map}_2 n' (\mathrm{map}_2 m_1 f g) (\mathrm{map}_2 m_2 f h)$$$
Lean4
/-- The other direction does not hold because of the `f-f` cross terms on the RHS. -/
theorem map₂_distrib_le_left {m : α → δ → ε} {n : β → γ → δ} {m₁ : α → β → β'} {m₂ : α → γ → γ'} {n' : β' → γ' → ε}
(h_distrib : ∀ a b c, m a (n b c) = n' (m₁ a b) (m₂ a c)) :
map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h) :=
by
rintro s ⟨t₁, ⟨u₁, hu₁, v, hv, ht₁⟩, t₂, ⟨u₂, hu₂, w, hw, ht₂⟩, hs⟩
refine ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂, _, image2_mem_map₂ hv hw, ?_⟩
refine (image2_distrib_subset_left h_distrib).trans ((image2_subset ?_ ?_).trans hs)
· exact (image2_subset_right inter_subset_left).trans ht₁
· exact (image2_subset_right inter_subset_right).trans ht₂
