and_right

Mathlib.Order.Minimal

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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