inter_eq_inter_iff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_eq_inter_iff_right : s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t :=
  inf_eq_inf_iff_right

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