sdiff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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