eq_of_subset — Mathlib

English

In the Maximal namespace, for P : Set α → Prop, s, t ⊆ α, if h : Maximal P s and ht : P t and hst : s ⊆ t, then t = s.

Русский

В области Maximal для P: Set α → Prop, s, t ⊆ α, если h : Maximal P s и ht : P t и hst: s ⊆ t, то t = s.

LaTeX

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

Lean4

theorem eq_of_subset (h : Maximal P s) (ht : P t) (hst : s ⊆ t) : s = t :=
  h.eq_of_le ht hst

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