subset — Mathlib

English

If t is PairwiseDisjoint under f and s ⊆ t, then s is PairwiseDisjoint under f.

Русский

Если t попарно непересекается относительно f и s ⊆ t, то s тоже попарно непересекается относительно f.

LaTeX

$$t.PairwiseDisjoint f \\Rightarrow s \\subseteq t \\Rightarrow s.PairwiseDisjoint f$$

Lean4

theorem subset (ht : t.PairwiseDisjoint f) (h : s ⊆ t) : s.PairwiseDisjoint f :=
  Pairwise.mono h ht

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