subset_insert_iff_of_notMem

Mathlib.Data.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.subset_insert_iff_of_notMem

English

If a is not in s, then s is a subset of insert a t if and only if s is a subset of t.

Русский

Если a ∉ s, то s ⊆ insert a t тогда и только тогда, когда s ⊆ t.

LaTeX

$$$ (a \\notin s) \\Rightarrow (s \\subseteq insert\\ a\\ t \\iff s \\subseteq t)$$$

Lean4

theorem subset_insert_iff_of_notMem (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t := by
  rw [subset_insert_iff, erase_eq_of_notMem h]

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

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

Разделы

Аффилиация

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