mul_def — Mathlib

English

Let x be an element of a directed direct limit. Then ⟦x⟧ equals 1 in the direct limit iff there exist i and h with f x.1 i h x.2 = 1.

Русский

Пусть x — элемент направленного пределa. Тогда ⟦x⟧ = 1 в пределе тогда и только тогда, когда существуют i и h такие, что f x.1 i h x.2 = 1.

LaTeX

$$$ \Big( \llbracket x \rrbracket = 1 \Big) \iff \exists i,h, f\,x.1\,i\,h\,x.2 = 1 $$$

Lean4

@[to_additive]
theorem mul_def (i) (x y : G i) : ⟦⟨i, x⟩⟧ * ⟦⟨i, y⟩⟧ = (⟦⟨i, x * y⟩⟧ : DirectLimit G f) :=
  map₂_def ..

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