copy — Mathlib

English

Copying a Boolean subalgebra L along a set s yields the same subalgebra provided s equals L.

Русский

Копирование булевой подпалгебры L по набору s возвращает ту же подпалгебру, если s равен L.

LaTeX

$$L.copy s hs = L$$

Lean4

/-- Copy of a Boolean subalgebra with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (L : BooleanSubalgebra α) (s : Set α) (hs : s = L) : BooleanSubalgebra α
    where
  toSublattice := L.toSublattice.copy s <| by subst hs; rfl
  compl_mem' := by subst hs; exact L.compl_mem'
  bot_mem' := by subst hs; exact L.bot_mem'

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