empty_notMem_disjointOfDiffUnion — Mathlib

English

The empty set is not a member of disjointOfDiffUnion.

Русский

Пустое множество не является элементом disjointOfDiffUnion.

LaTeX

$$$$ ∅ \\\\notin hC.disjointOfDiffUnion hs hI $$$$

Lean4

theorem empty_notMem_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    ∅ ∉ hC.disjointOfDiffUnion hs hI := by
  classical simp only [disjointOfDiffUnion, mem_sdiff, Finset.mem_singleton, not_true, and_false, not_false_iff]

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