disjoint_toSubmodule — Mathlib

English

Disjointness of LieSubmodules corresponds to disjointness of their underlying Submodules.

Русский

Расстояние между подподмодулями Ли соответствует расстоянию между их подмодулями как обычными подмодулями.

LaTeX

$$$\text{Disjoint}(N,N') \;\Longleftrightarrow\; \text{Disjoint}(N^{\text{toSubmodule}}, N'^{\text{toSubmodule}})$$$

Lean4

@[simp]
theorem disjoint_toSubmodule : Disjoint (N : Submodule R M) (N' : Submodule R M) ↔ Disjoint N N' := by
  rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule, ← disjoint_iff]

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