div_inter_subset — Mathlib

English

Let α be a type equipped with a binary operation “division”. For any finite sets s, t1, t2 ⊆ α, every quotient obtainable from s by elements of t1 ∩ t2 also arises as a quotient using t1 and also as a quotient using t2. In symbols, { x/y : x ∈ s, y ∈ t1 ∩ t2 } ⊆ { x/y : x ∈ s, y ∈ t1 } ∩ { x/y : x ∈ s, y ∈ t2 }.

Русский

Пусть α — множество с бинарной операцией деления. Для любых конечных множеств s, t1, t2 ⊆ α множество частных элементов { x/y : x ∈ s, y ∈ t1 ∩ t2 } является подмножеством пересечения { x/y : x ∈ s, y ∈ t1 } и { x/y : x ∈ s, y ∈ t2 }.

LaTeX

$$$$ s /(t_1 \\cap t_2) \\subseteq s / t_1 \\cap (s / t_2) $$$$

Lean4

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

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