inter_div_subset — Mathlib

English

The image of the intersection under division by t is contained in the intersection of the quotients: s1 ∩ s2 / t ⊆ (s1 / t) ∩ (s2 / t).

Русский

Образ пересечения под делением на t содержится в пересечении делений: (s1 ∩ s2) / t ⊆ (s1 / t) ∩ (s2 / t).

LaTeX

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

Lean4

@[to_additive]
theorem inter_div_subset : s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t) :=
  image₂_inter_subset_left

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