ssubset_union_left_iff

Mathlib.Data.Set.Basic

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

English

s ⊂ s ∪ t ↔ ¬ (t ⊆ s).

Русский

s ⊂ s ∪ t эквивалентно тому, что t ⊄ s

LaTeX

$$$s \subset s \cup t \iff \neg (t \subseteq s)$$$

Lean4

@[simp]
theorem ssubset_union_left_iff : s ⊂ s ∪ t ↔ ¬t ⊆ s :=
  left_lt_sup

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

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

Разделы

Аффилиация

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