isLowerSet_preimage_coe — Mathlib

English

If s is an upper set, then the preimage of t under the inclusion into s is a lower set, and this holds iff for all b ∈ s and c ∈ t with b ≤ c we have b ∈ t.

Русский

Если s — верхнее множество, то прообраз t по включению в s является нижним множеством, и это эквивалентно условию: для всех b ∈ s, c ∈ t, если b ≤ c, то b ∈ t.

LaTeX

$$$IsUpperSet(s) \\to \\bigl(IsLowerSet\\bigl((\\uparrow)^{-1} t : Set\\ s\\bigr) \\iff \\forall b \\in s, \\forall c \\in t, b \\le c \\to b \\in t\\bigr)$$$

Lean4

theorem isLowerSet_preimage_coe (hs : IsUpperSet s) :
    IsLowerSet ((↑) ⁻¹' t : Set s) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t := by aesop

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