inclusion_right

Mathlib.Data.Set.Inclusion

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

English

For h: s ⊆ t, x ∈ t, and m: x ∈ s, inclusion(h)⟨x, m⟩ = x.

Русский

Для h: s ⊆ t, x ∈ t и m: x ∈ s, включение(h)⟨x, m⟩ = x.

LaTeX

$$$\forall (h: s \subseteq t)\, (x: t)\, (m: (x : \alpha) \in s),\ inclusion(h)\langle x, m \rangle = x.$$$

Lean4

theorem inclusion_right (h : s ⊆ t) (x : t) (m : (x : α) ∈ s) : inclusion h ⟨x, m⟩ = x :=
  by
  cases x
  rfl

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

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

Разделы

Аффилиация

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