inclusion — Mathlib

English

The inclusion from H to K exists whenever H ≤ K.

Русский

Существует включение из H в K, если H ≤ K.

LaTeX

$$$H \le K \Rightarrow \text{inclusion}_{H\to K} : H \to K \text{ является моноид-гомоморфизм}$$$

Lean4

/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
@[to_additive /-- The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`. -/
    ]
def inclusion {H K : Subgroup G} (h : H ≤ K) : H →* K :=
  MonoidHom.mk' (fun x => ⟨x, h x.2⟩) fun _ _ => rfl

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