and_right

Mathlib.Order.Minimal

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

English

If x is maximal for P and Q holds, then x is maximal for P ∧ Q.

Русский

Если x максимален относительно P и Q верно, то x максимален относительно P ∧ Q.

LaTeX

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

Lean4

theorem and_right (h : Maximal P x) (hQ : Q x) : Maximal (fun x ↦ (P x ∧ Q x)) x :=
  h.mono (fun _ ↦ And.left) ⟨h.prop, hQ⟩

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

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

Разделы

Аффилиация

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