coe_toSet_mk — Mathlib

English

The underlying set of the constructed LieSubmodule equals the original set S.

Русский

Множественный носитель сконструированного подмодуля Ли равен исходному множеству S.

LaTeX

$$$ ((\langle\langle\langle\langle S, h_1 \rangle, h_2 \rangle, h_3 \rangle, h_4 \rangle : LieSubmodule R L M) : Set M) = S $$$

Lean4

@[simp]
theorem coe_toSet_mk (S : Set M) (h₁ h₂ h₃ h₄) : ((⟨⟨⟨⟨S, h₁⟩, h₂⟩, h₃⟩, h₄⟩ : LieSubmodule R L M) : Set M) = S :=
  rfl

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