disjoint_supported_supported_iff — Mathlib

English

Under a nontrivial M, disjointness of supports is equivalent to disjointness of the index sets.

Русский

При ненулевом M раздельность опор эквивалентна раздельности самих множеств.

LaTeX

$$$[\text{Nontrivial } M] \Rightarrow (\mathrm{Disjoint}(\mathrm{supported}(M,R,s), \mathrm{supported}(M,R,t)) \iff \mathrm{Disjoint}(s,t))$$$

Lean4

theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} :
    Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t :=
  by
  refine ⟨fun h => Set.disjoint_left.mpr fun x hx1 hx2 => ?_, disjoint_supported_supported⟩
  rcases exists_ne (0 : M) with ⟨y, hy⟩
  have := h.le_bot ⟨single_mem_supported R y hx1, single_mem_supported R y hx2⟩
  rw [mem_bot, single_eq_zero] at this
  exact hy this

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