notMem_disjointOfDiff — Mathlib

English

For s,t ∈ C, the set t is not an element of hC.disjointOfDiff hs ht.

Русский

Для s,t ∈ C множество t не является элементом hC.disjointOfDiff hs ht.

LaTeX

$$$$ t \\\\notin hC.disjointOfDiff hs ht $$$$

Lean4

theorem notMem_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : t ∉ hC.disjointOfDiff hs ht :=
  by
  intro hs_mem
  suffices t ⊆ s \ t by
    have h := @disjoint_sdiff_self_right _ t s _
    specialize h le_rfl this
    simp only [Set.bot_eq_empty, Set.le_eq_subset, subset_empty_iff] at h
    refine hC.empty_notMem_disjointOfDiff hs ht ?_
    rwa [← h]
  rw [← hC.sUnion_disjointOfDiff hs ht]
  exact subset_sUnion_of_mem hs_mem

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