subset

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Eq.subset

← MathLib Explorer

English

If two sets s and t are equal, then s is a subset of t.

Русский

Если множества s и t равны, то s ⊆ t.

LaTeX

$$$s = t \rightarrow s \subseteq t$$$

Lean4

/-- Duplicate of `Eq.subset'`, which currently has elaboration problems. -/
theorem subset {α} {s t : Set α} : s = t → s ⊆ t := fun h₁ _ h₂ => by rw [← h₁]; exact h₂

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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