instSetLikeHomogeneousSubmodule — Mathlib

English

There is a SetLike structure on the collection of homogeneous submodules, with the underlying set being the submodule itself.

Русский

У множества однородных подмодулей существует структура SetLike, где подмодуль является основанием множества.

LaTeX

$$$$ \text{SetLike}(\text{HomogeneousSubmodule } 𝒜 \ ℳ, M). $$$$

Lean4

instance : SetLike (HomogeneousSubmodule 𝒜 ℳ) M
    where
  coe X := X.toSubmodule
  coe_injective' := by
    rintro ⟨p, hp⟩ ⟨q, hq⟩ (h : (p : Set M) = q)
    simpa using h

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