minimal_and_iff_left_of_imp — Mathlib

English

If P implies Q for all x, then Minimal (Q x ∧ P x) x is equivalent to Q x ∧ Minimal P x.

Русский

Если P для всех x имплицирует Q, тогда Minimal (Q x ∧ P x) x эквивалентно Q x ∧ Minimal P x.

LaTeX

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

Lean4

theorem minimal_and_iff_left_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) : Minimal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ (Minimal P x) := by
  simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]

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