disjoint_of_subset_left — Mathlib

English

Let s, t, u be finite subsets such that s ⊆ u and u is disjoint from t. Then s is disjoint from t as well; equivalently, if s ⊆ u and s ∩ t ≠ ∅ would imply u ∩ t ≠ ∅, which contradicts disjointness.

Русский

Пусть s, t, u — конечные подмножества; если s ⊆ u и u ∩ t = ∅, то s ∩ t = ∅; иными словами, непересечение сохраняется при включении подмножества.

LaTeX

$$$s \\subseteq u \\land (u \\cap t) = \\varnothing \\Rightarrow (s \\cap t) = \\varnothing$$$

Lean4

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

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