English
The symmetric right-hand inequality: under a distributive hypothesis, map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h).
Русский
Симметричное неравенство справа: при условии распределимости имеем map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h).
LaTeX
$$$\mathrm{map}_2 m (\mathrm{map}_2 n f g) h \le \mathrm{map}_2 n' (\mathrm{map}_2 m_1 f h) (\mathrm{map}_2 m_2 g h)$$$
Lean4
/-- The other direction does not hold because of the `h`-`h` cross terms on the RHS. -/
theorem map₂_distrib_le_right {m : δ → γ → ε} {n : α → β → δ} {m₁ : α → γ → α'} {m₂ : β → γ → β'} {n' : α' → β' → ε}
(h_distrib : ∀ a b c, m (n a b) c = n' (m₁ a c) (m₂ b c)) :
map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h) :=
by
rintro s ⟨t₁, ⟨u, hu, w₁, hw₁, ht₁⟩, t₂, ⟨v, hv, w₂, hw₂, ht₂⟩, hs⟩
refine ⟨_, image2_mem_map₂ hu hv, w₁ ∩ w₂, inter_mem hw₁ hw₂, ?_⟩
refine (image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)
· exact (image2_subset_left inter_subset_left).trans ht₁
· exact (image2_subset_left inter_subset_right).trans ht₂
