maximal_subtype — Mathlib

English

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

Русский

Для элемента x из подтипа Q максимальность P на x.1 эквивалентна максимальности P ∧ Q на x в подтипе.

LaTeX

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

Lean4

@[simp]
theorem maximal_subtype {x : Subtype Q} : Maximal (fun x ↦ P x.1) x ↔ Maximal (P ⊓ Q) x :=
  minimal_subtype (α := αᵒᵈ)

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