or — Mathlib · SciLib

English

If x is minimal for P ∨ Q, then x is minimal for P or x is minimal for Q.

Русский

Если x минимально для P ∨ Q, то x минимально для P или минимально для Q.

LaTeX

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

Lean4

theorem or (h : Minimal (fun x ↦ P x ∨ Q x) x) : Minimal P x ∨ Minimal Q x :=
  by
  obtain ⟨h | h, hmin⟩ := h
  · exact .inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩
  exact .inr ⟨h, fun y hy hyx ↦ hmin (Or.inr hy) hyx⟩

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