infs_eq_empty

Mathlib.Data.Set.Sups

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

English

s ⊼ t = ∅ iff s = ∅ or t = ∅.

Русский

s ⊼ t = ∅ тогда и только тогда, когда s = ∅ или t = ∅.

LaTeX

$$$ s \⊼ t = \emptyset \iff s = \emptyset \lor t = \emptyset $$$

Lean4

@[simp]
theorem infs_eq_empty : s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image2_eq_empty_iff

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

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

Разделы

Аффилиация

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