insert_subset

Mathlib.Data.Set.Insert

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

English

If a ∈ t and s ⊆ t, then insert a s ⊆ t.

Русский

Пусть a ∈ t и s ⊆ t. Тогда insert a s ⊆ t.

LaTeX

$$$(a \in t) \land (s \subseteq t) \Rightarrow (s \cup \{a\}) \subseteq t$$$

Lean4

theorem insert_subset (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t := by grind

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

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

Разделы

Аффилиация

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