inclusion_mk

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.inclusion_mk

English

The inclusion map respects the canonical representatives: inclusion h (⟨x, hx⟩) = ⟨x, h hx⟩.

Русский

Включение сохраняет канонические представления: включение h (⟨x, hx⟩) = ⟨x, h hx⟩.

LaTeX

$$$\text{inclusion}(h)(\langle x, hx \rangle) = \langle x, h hx \rangle$$$

Lean4

@[simp]
theorem inclusion_mk (x : A) (hx : x ∈ S) : inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru