coe_inf — Mathlib

English

The underlying Submodule of the infimum equals the intersection of the underlying Submodules.

Русский

Подмодуль-подмножество, полученный как пересечение инфимума, совпадает с пересечением соответствующих подмодулей.

LaTeX

$$$ (\,N \\ N' : LieSubmodule R L M) : (↑(N \sqcap N') : Submodule R M) = ↑N \cap ↑N' $$$

Lean4

@[simp]
theorem coe_inf : (↑(N ⊓ N') : Set M) = ↑N ∩ ↑N' :=
  rfl

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