inter_eq_left

Mathlib.Data.Set.Basic

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

English

Let S and T be sets. The equality S ∩ T = S holds exactly when S is contained in T.

Русский

Пусть S и T — множества. Равенство S ∩ T = S верно тогда и только тогда, когда S ⊆ T.

LaTeX

$$$S \cap T = S \iff S \subseteq T$$$

Lean4

@[simp]
theorem inter_eq_left : s ∩ t = s ↔ s ⊆ t :=
  inf_eq_left

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

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

Разделы

Аффилиация

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