subset_disjointOfDiff — Mathlib

English

Every block appearing in the disjoint decomposition of s \ t belongs to C.

Русский

Каждый элемент разложения s \ t по блокам принадлежит C.

LaTeX

$$$\forall A\in hC.disjointOfDiff\; hs\; ht,\ A\in C.$$$

Lean4

theorem subset_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : ↑(hC.disjointOfDiff hs ht) ⊆ C := by
  classical
  simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
  exact (hC.diff_eq_sUnion' s hs t ht).choose_spec.1.trans (Set.subset_insert _ _)

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