ssubset_union_right_iff

Mathlib.Data.Set.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ssubset_union_right_iff : t ⊂ s ∪ t ↔ ¬s ⊆ t :=
  right_lt_sup

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

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

Разделы

Аффилиация

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