infs_subset_iff

Mathlib.Data.Set.Sups

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

English

The infimum of two nonempty sets is nonempty.

Русский

Наименьшее нижнее ограничение двух непустых множеств остаётся непустым.

LaTeX

$$$ (s \⊼ t).Nonempty \iff s.Nonempty \land t.Nonempty $$$

Lean4

@[simp]
theorem infs_subset_iff : s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u :=
  image2_subset_iff

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

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

Разделы

Аффилиация

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