English
Let f: I → Submodule R M and g: J → Submodule R M be two families of submodules. The colon of the infimum of the f(i) with the supremum of the g(j) equals the infimum over all i, j of the colon: (⊓_i f(i)) : (⊔_j g(j)) = ⊓_{i,j} (f(i) : (g(j))).
Русский
Пусть f и g — семейства подмодулей; колонна пересечения f(i) по объединению g(j) равна пересечению по всем парам (i, j) колонн.
LaTeX
$$$\\Big(\\bigwedge_i f_i\\Big) : (\\bigvee_j g_j) = \\bigwedge_{i,j} (f_i : g_j)$$$
Lean4
theorem iInf_colon_iSup (ι₁ : Sort*) (f : ι₁ → Submodule R M) (ι₂ : Sort*) (g : ι₂ → Submodule R M) :
(⨅ i, f i).colon (⨆ j, g j) = ⨅ (i) (j), (f i).colon (g j) :=
le_antisymm (le_iInf fun _ => le_iInf fun _ => colon_mono (iInf_le _ _) (le_iSup _ _)) fun _ H =>
mem_colon'.2 <|
iSup_le fun j =>
map_le_iff_le_comap.1 <|
le_iInf fun i =>
map_le_iff_le_comap.2 <|
mem_colon'.1 <|
have := (mem_iInf _).1 H i
have := (mem_iInf _).1 this j
this
