pairwise_disjoint_mono — Mathlib

English

If a family is pairwise disjoint, and g ≤ f, then the family g is also pairwise disjoint.

Русский

Если семейство попарно непересекается, и g ≤ f, то семейство g также попарно непересекается.

LaTeX

$$$ \text{Pairwise}(\operatorname{Disjoint} \circ f) \land g \le f \Rightarrow \text{Pairwise}(\operatorname{Disjoint} \circ g) $$$

Lean4

theorem pairwise_disjoint_mono [PartialOrder α] [OrderBot α] (hs : Pairwise (Disjoint on f)) (h : g ≤ f) :
    Pairwise (Disjoint on g) :=
  hs.mono fun i j hij => Disjoint.mono (h i) (h j) hij

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