inclusion_injective

Mathlib.Data.Set.Inclusion

URI: https://scilib.ai/kg/mathlib#Set.inclusion_injective

English

For h: s ⊆ t, the inclusion map i_h: s → t is injective.

Русский

Для h: s ⊆ t включение i_h: s → t является инъекцией.

LaTeX

$$$\text{Injective}(\mathrm{inclusion}(h)).$$$

Lean4

theorem inclusion_injective (h : s ⊆ t) : Injective (inclusion h)
  | ⟨_, _⟩, ⟨_, _⟩ => Subtype.ext_iff.2 ∘ Subtype.ext_iff.1

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

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

Разделы

Аффилиация

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