or

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#Maximal.or

English

If x is maximal for P ∨ Q, then x is maximal for P or x is maximal for Q.

Русский

Если x максимален для P ∨ Q, то x максимален для P или для Q.

LaTeX

$$$\\text{Maximal}(P \\lor Q)\\, x \\to \\text{Maximal } P\\, x \\lor \\text{Maximal } Q\\, x$$$

Lean4

theorem or (h : Maximal (fun x ↦ P x ∨ Q x) x) : Maximal P x ∨ Maximal Q x :=
  Minimal.or (α := αᵒᵈ) h

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

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

Разделы

Аффилиация

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