isUpperSet_preimage_coe — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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