inf_iInf

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#Submodule.inf_iInf

← MathLib Explorer

English

q ⊓ ⨅ i, p(i) = ⨅ i, q ⊓ p(i).

Русский

q ∧ (∧_i p(i)) = ∧_i (q ∧ p(i)).

LaTeX

$$$q \wedge (\bigwedge_i p_i) = \bigwedge_i (q \wedge p_i)$$$

Lean4

theorem inf_iInf {ι : Sort*} [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M) : q ⊓ ⨅ i, p i = ⨅ i, q ⊓ p i :=
  SetLike.coe_injective <| by simpa only [coe_inf, coe_iInf] using Set.inter_iInter _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru