minimal_and_iff_right_of_imp — Mathlib

English

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

Русский

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

LaTeX

$$$\\bigl(\\forall x, P(x) \\to Q(x)\\bigr) \\to \\text{Minimal}(x \\mapsto P(x) \\land Q(x))\\, x \\iff (\\text{Minimal } P\\, x) \\land Q x$$$

Lean4

theorem minimal_and_iff_right_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) : Minimal (fun x ↦ P x ∧ Q x) x ↔ (Minimal P x) ∧ Q x :=
  by
  simp_rw [and_iff_left_of_imp (fun x ↦ hPQ x), iff_self_and]
  exact fun h ↦ hPQ h.prop

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