lowerClosure_sup_sdiff — Mathlib

English

Let s be a lower set and t a set with t ⊆ s, and suppose that for every b ∈ s and every c ∈ t, if c ≤ b then b ∈ t. Then the join of lowerClosure(t) and s \ t equals s; in other words, s is generated by t and the part of s outside t.

Русский

Пусть s — нижнее множество, t — множество с t ⊆ s, и предположим, что для любых b ∈ s и c ∈ t, если c ≤ b, то b ∈ t. Тогда объединение нижнего замыкания t и множества s \ t даёт s; то есть s порождается t и тем, что лежит вне t.

LaTeX

$$$\\operatorname{lowerClosure}(t) \\sqcup (s \\setminus t) = s$$$

Lean4

theorem lowerClosure_sup_sdiff (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) : lowerClosure t ⊔ s.sdiff t = s :=
  by rw [sup_comm, sdiff_sup_lowerClosure hts hst]

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