pair_subset

Mathlib.Data.Set.Insert

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

English

If a and b belong to s, then {a, b} is a subset of s.

Русский

Если a и b принадлежат s, то {a, b} ⊆ s.

LaTeX

$$$(a \\in s) \\land (b \\in s) \\Rightarrow \\{a,b\\} \\subseteq s$$$

Lean4

theorem pair_subset (ha : a ∈ s) (hb : b ∈ s) : { a, b } ⊆ s :=
  pair_subset_iff.2 ⟨ha, hb⟩

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

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

Разделы

Аффилиация

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