isMaximal — Mathlib

English

A complete type p over theory T is maximal in the lattice of theories: the corresponding theory is maximal.

Русский

Полный тип p над теорией T является максимальным в частичной упорядоченной системе теорий: соответствующая теория максимальна.

LaTeX

$$$IsMaximal(p : L[[\\alpha]].Theory)$$$

Lean4

theorem isMaximal (p : T.CompleteType α) : IsMaximal (p : L[[α]].Theory) :=
  p.isMaximal'

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