and_left

Mathlib.Order.Minimal

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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