copy — Mathlib

English

Copying an intermediate field with the same carrier yields the same intermediate field.

Русский

Копирование промежуточного поля с тем же носителем приводит к тому же самому полю.

LaTeX

$$$S.copy(s, hs) = S \quad \text{whenever } hs : s = \uparrow S$$$

Lean4

/-- Copy of an intermediate field with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (S : IntermediateField K L) (s : Set L) (hs : s = ↑S) : IntermediateField K L
    where
  toSubalgebra := S.toSubalgebra.copy s hs
  inv_mem' := hs.symm ▸ S.inv_mem'

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