pairwiseDisjoint — Mathlib

English

If f ≤ g pointwise on s, and s is SupIndep, then f is SupIndep whenever g is SupIndep.

Русский

Если f ≤ g по всем точкам на s, и s SupIndep, то f SupIndep при g.

LaTeX

$$$\\text{SuppIndep}(s,f) \\Rightarrow \\text{SuppIndep}(s,g) \\text{ if } f(x) \\le g(x) \\text{ for all } x \\in s.$$$

Lean4

theorem pairwiseDisjoint (hs : s.SupIndep f) : (s : Set ι).PairwiseDisjoint f := fun _ ha _ hb hab =>
  sup_singleton.subst <| hs (singleton_subset_iff.2 hb) ha <| notMem_singleton.2 hab

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