disjSups_inter_subset_left — Mathlib

English

The infimum of an intersection distributes as subset: (s1 ∩ s2) ○ t ⊆ (s1 ○ t) ∩ (s2 ○ t).

Русский

Инфимум пересечения распределяется как подмножество: (s1 ∩ s2) ○ t ⊆ (s1 ○ t) ∩ (s2 ○ t).

LaTeX

$$$ (s_{1} \cap s_{2}) \circ t \subseteq (s_{1} \circ t) \cap (s_{2} \circ t) $$$

Lean4

theorem disjSups_inter_subset_left : (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t := by
  simpa only [disjSups, inter_product, filter_inter_distrib] using image_inter_subset _ _ _

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