minimal_subtype — Mathlib

English

For an element x of a subtype Q, minimality of P applied to the base component x.1 is equivalent to minimality of the conjunction P ∧ Q on x within the subtype.

Русский

Для элемента x из подтипа Q минимум P, применённый к основанию x.1, эквивалентен минимуму P ∧ Q на x в подтипе.

LaTeX

$$$\\text{Minimal}(\\lambda x, P\,x.1)\\, x \\iff \\text{Minimal}(P \\land Q)\\, x$$$

Lean4

@[simp]
theorem minimal_subtype {x : Subtype Q} : Minimal (fun x ↦ P x.1) x ↔ Minimal (P ⊓ Q) x :=
  by
  obtain ⟨x, hx⟩ := x
  simp only [Minimal, Subtype.forall, Subtype.mk_le_mk, Pi.inf_apply, inf_Prop_eq]
  tauto

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