disjoint_of_subset_right — Mathlib

English

If t ⊆ u and s is disjoint from u, then s is disjoint from t. Disjointness is preserved when restricting the second set to a subset.

Русский

Пусть t ⊆ u и s декартово не пересекается с u, тогда s не пересекается с t; сохраняется свойство непересечения при ограничении множества на подмножество.

LaTeX

$$$t \\subseteq u \\land \\operatorname{Disjoint}(s,u) \\Rightarrow \\operatorname{Disjoint}(s,t)$$$

Lean4

theorem disjoint_of_subset_right (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t :=
  disjoint_right.2 fun _x m₁ => (disjoint_right.1 d) (h m₁)

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