closure — Mathlib

English

A Finite-index biUnion of semilinear sets is semilinear.

Русский

Финитный biUnion полей семилинейных множеств сохраняет семилинейность.

LaTeX

$$$biUnion Finset \to IsSemilinearSet\ toIsSemilinearSet(⋃ i ∈ s, t i).$$$

Lean4

/-- Semilinear sets are closed under additive closure. -/
protected theorem closure (hs : IsSemilinearSet s) : IsSemilinearSet (closure s : Set M) :=
  by
  rcases hs with ⟨S, hS, hS', rfl⟩
  induction S, hS using Finite.induction_on with
  | empty => simp
  | insert S _ ih =>
    simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa [closure_union, coe_sup] using hS'.1.closure.add (ih hS'.2)

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