not_ssuperset — Mathlib

English

Let P be a predicate on subsets. If s is maximal with respect to P and P(t) holds for some t, then s is not a strict subset of t; i.e., no t properly contains s while still satisfying P.

Русский

Пусть P — свойство подмножеств; если s максимальна по P, и существует t с P(t), то не существует строгого надмножества t такого, что s ⊊ t.

LaTeX

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

Lean4

theorem not_ssuperset (h : Maximal P s) (ht : P t) : ¬s ⊂ t :=
  h.not_gt ht

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