eq_of_le — Mathlib

English

Let l be the lower adjoint to the inclusion i: α → Set β. If s is a subset of β contained in i(S) for some S ∈ α, and S ≤ l(s) in α, then l(s) = S.

Русский

Пусть l — нижнее сопряжение к включению i: α → Set β. Пусть s ⊆ β содержится в i(S) для некоторого S ∈ α, и S ≤ l(s) по порядку в α. Тогда l(s) = S.

LaTeX

$$$\forall s:\ Set\beta, \forall S:\alpha, \ s \subseteq (↑S) \land S \le l(s) \Rightarrow l(s) = S$$$

Lean4

theorem eq_of_le {s : Set β} {S : α} (h₁ : s ⊆ S) (h₂ : S ≤ l s) : l s = S :=
  ((l.le_iff_subset _ _).2 h₁).antisymm h₂

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