infs_sups_subset_left

Mathlib.Data.Set.Sups

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

English

Distributive property: s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u.

Русский

Свойство дистрибутивности: s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u.

LaTeX

$$$s \\⊼ (t \\⊻ u) \\subseteq s \\⊼ t \\⊻ s \\⊼ u$$$

Lean4

theorem infs_sups_subset_left : s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u :=
  image2_distrib_subset_left inf_sup_left

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

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

Разделы

Аффилиация

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