sups_inter_subset_left — Mathlib

English

The sups of an intersection subset is contained in the intersection of sups: (s₁ ∩ s₂) ⊻ t ⊆ (s₁ ⊻ t) ∩ (s₂ ⊻ t).

Русский

Супы пересечения множитво содержатся в пересечении супов: (s₁ ∩ s₂) ⊻ t ⊆ (s₁ ⊻ t) ∩ (s₂ ⊻ t).

LaTeX

$$$ (s_1 \cap s_2) \oplus t \subseteq (s_1 \oplus t) \cap (s_2 \oplus t) $$$

Lean4

theorem sups_inter_subset_left : (s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t :=
  image₂_inter_subset_left

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