forall_infs_iff

Mathlib.Data.Set.Sups

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

English

The inclusion s ⊼ t ⊆ u holds iff ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u.

Русский

Проверка включения s ⊼ t ⊆ u эквивалентна тому, что ∀ a ∈ s и ∀ b ∈ t, a ⊓ b ∈ u.

LaTeX

$$$ s ⊼ t \subseteq u \iff \forall a \in s, \forall b \in t, a \wedge b \in u $$$

Lean4

theorem forall_infs_iff {p : α → Prop} : (∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b) :=
  forall_mem_image2

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

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

Разделы

Аффилиация

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