eq_of_superset — Mathlib

English

In the Maximal namespace, for P : Set α → Prop, s, t ⊆ α, Maximal P s and P t and s ⊆ t imply t ⊆ s, hence t = s.

Русский

В пространстве Maximal, для P : Set α → Prop, s, t ⊆ α, Maximal P s и P t и s ⊆ t приводят к t ⊆ s, следовательно t = s.

LaTeX

$$$$ \\text{Maximal } P s \\land P t \\land s \\subseteq t \\;\\Rightarrow\\; t \\subseteq s. $$$$

Lean4

theorem eq_of_superset (h : Maximal P s) (ht : P t) (hst : s ⊆ t) : t = s :=
  h.eq_of_ge ht hst

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