isSetSemiring — Mathlib

English

If C is a ring of sets, then it is a semiring of sets.

Русский

Если C — кольцо множеств, то оно является полукольцом множеств.

LaTeX

$$$\text{IsSetRing}(C) \Rightarrow \text{IsSetSemiring}(C).$$$

Lean4

theorem isSetSemiring (hC : IsSetRing C) : IsSetSemiring C
    where
  empty_mem := hC.empty_mem
  inter_mem := fun _ hs _ ht => hC.inter_mem hs ht
  diff_eq_sUnion' := by
    refine fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩
    · simp only [coe_singleton, Set.singleton_subset_iff]
      exact hC.diff_mem hs ht
    · simp only [coe_singleton, pairwiseDisjoint_singleton]
    · simp only [coe_singleton, sUnion_singleton]

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