not_prop_of_ssuperset — Mathlib

English

Let P be a predicate on subsets of a set X. If s is maximal with respect to P, then no proper superset t of s satisfies P; i.e., for every t with s ⊊ t, not P(t).

Русский

Пусть P — некое свойство подмножеств множества X. Пусть s максимальна по P; тогда не существует строгого надмножества t => P(t) не выполняется, то есть для любого t, удовлетворяющего s ⊊ t, выполняется ¬P(t).

LaTeX

$$$\\forall S,T\\subseteq X,\\; (\\text{Maximal } P\\, S) \\to (S \\subsetneq T) \\to \\lnot P(T).$$$

Lean4

theorem not_prop_of_ssuperset (h : Maximal P s) (ht : s ⊂ t) : ¬P t :=
  (maximal_iff_forall_gt.1 h).2 ht

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