integerSetToAssociates_apply — Mathlib

English

The simplification applies: integerSetToAssociates K a = ⟦preimageOfMemIntegerSet a⟧ for any a in integerSet K.

Русский

Упрощение: для любого a ∈ integerSet K имеем integerSetToAssociates K a = ⟦preimageOfMemIntegerSet a⟧.

LaTeX

$$$\\operatorname{integerSetToAssociates} \\, K \\, a = \\llbracket \\operatorname{preimageOfMemIntegerSet}(a) \\rrbracket.$$$

Lean4

@[simp]
theorem integerSetToAssociates_apply (a : integerSet K) : integerSetToAssociates K a = ⟦preimageOfMemIntegerSet a⟧ :=
  rfl

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