inter_eq_inter_iff_left — Mathlib

English

For finite sets S, T, U, we have S ∩ T = S ∩ U if and only if S ∩ U ⊆ T and S ∩ T ⊆ U.

Русский

Для конечных множеств S, T, U верно S ∩ T = S ∩ U тогда и только тогда, когда S ∩ U ⊆ T и S ∩ T ⊆ U.

LaTeX

$$$ (S \\cap T) = (S \\cap U) \\\\iff (S \\cap U \\subseteq T) \\land (S \\cap T \\subseteq U) $$$

Lean4

theorem inter_eq_inter_iff_left : s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u :=
  inf_eq_inf_iff_left

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