sdiff — Mathlib

English

If s is an upper set and, whenever b ∈ s and c ∈ t with b ≤ c we have b ∈ t, then s \ t is upper.

Русский

Если s — верхнее множество и при любых b ∈ s и c ∈ t с b ≤ c выполняется b ∈ t, то s \ t — верхнее множество.

LaTeX

$$$IsUpperSet(s) \\to \\bigl(\\forall b \\in s, \\forall c \\in t, b \\le c \\to b \\in t\\bigr) \\to IsUpperSet(s \\setminus t)$$$

Lean4

theorem sdiff (hs : IsUpperSet s) (ht : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) : IsUpperSet (s \ t) := fun _b _c hbc hb ↦
  ⟨hs hbc hb.1, fun hc ↦ hb.2 <| ht _ hb.1 _ hc hbc⟩

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