le_iff

Mathlib.ModelTheory.Definability

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.DefinableSet.le_iff

English

Every x ∈ α → M belongs to the top definable set.

Русский

Любой элемент функций α → M принадлежит верхнему определяемому множеству.

LaTeX

$$$$ x \\in (\\top : L.DefinableSet A α) $$$$

Lean4

theorem le_iff : s ≤ t ↔ (s : Set (α → M)) ≤ (t : Set (α → M)) :=
  Iff.rfl

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

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

Разделы

Аффилиация

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