empty_notMem_disjointOfDiff — Mathlib

English

The empty set is not one of the pieces in the disjoint decomposition of s \ t.

Русский

Пустое множество не входит в разложение разности s \ t на элементы C.

LaTeX

$$$\emptyset \not\in hC.disjointOfDiff\; hs\; ht$$$

Lean4

theorem empty_notMem_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : ∅ ∉ hC.disjointOfDiff hs ht := by
  classical simp only [disjointOfDiff, mem_sdiff, Finset.mem_singleton, not_true, and_false, not_false_iff]

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