inclusion_eq_id

Mathlib.Data.Set.Inclusion

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

English

If h is a subset relation of s into itself, the inclusion map equals the identity on s.

Русский

Если h: s ⊆ s, то включение h равно тождественному отображению на s.

LaTeX

$$$\forall h: s \subseteq s,\ inclusion(h) = \mathrm{id}_s.$$$

Lean4

theorem inclusion_eq_id (h : s ⊆ s) : inclusion h = id :=
  funext inclusion_self

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

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

Разделы

Аффилиация

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