inter_congr_right

Mathlib.Data.Finset.Lattice.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_congr_right (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t ∩ u :=
  inf_congr_right hs ht

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

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

Разделы

Аффилиация

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