notMem_of_mem_powerset_of_notMem — Mathlib

English

If a is not in s, then every subset t of s (i.e., t ∈ powerset(s)) also does not contain a.

Русский

Если a не принадлежит s, то каждый элемент t подмножества s также не содержит a.

LaTeX

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

Lean4

theorem notMem_of_mem_powerset_of_notMem {s t : Finset α} {a : α} (ht : t ∈ s.powerset) (h : a ∉ s) : a ∉ t :=
  by
  apply mt _ h
  apply mem_powerset.1 ht

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