inter_congr_right

Mathlib.Data.Set.Basic

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

English

If T ∩ U ⊆ S and S ∩ U ⊆ T, then S ∩ U = T ∩ U.

Русский

Если T ∩ U ⊆ S и S ∩ U ⊆ T, то S ∩ U = T ∩ U.

LaTeX

$$(T ∩ U ⊆ S) ∧ (S ∩ U ⊆ T) ⇒ S ∩ U = T ∩ 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