inter_congr_left

Mathlib.Data.Finset.Lattice.Basic

URI: https://scilib.ai/kg/mathlib#Finset.inter_congr_left

English

Let S, T, U be finite sets. If S ∩ U ⊆ T and S ∩ T ⊆ U, then S ∩ T = S ∩ U.

Русский

Пусть S, T, U — конечные множества. Если S ∩ U ⊆ T и S ∩ T ⊆ U, то S ∩ T = S ∩ U.

LaTeX

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

Lean4

theorem inter_congr_left (ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) : s ∩ t = s ∩ u :=
  inf_congr_left ht hu

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru