eq_of_superset — Mathlib

English

In the Minimal namespace, for P : Set α → Prop, s, t ⊆ α, if s is minimal with respect to P, and t ⊆ s with P t, then s = t.

Русский

В области Minimal для P: Set α → Prop, если s минимально среди множеств с свойством P, и t ⊆ s с P t, то s = t.

LaTeX

$$$$ \\text{Minimal } P s \\;\\Longrightarrow\\; P t \\land t \\subseteq s \\;\\Longrightarrow\\; s = t. $$$$

Lean4

theorem eq_of_superset (h : Minimal P s) (ht : P t) (hts : t ⊆ s) : s = t :=
  h.eq_of_ge ht hts

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