ofEquiv_σ

Mathlib.Data.Analysis.Filter

URI: https://scilib.ai/kg/mathlib#Filter.Realizer.ofEquiv_σ

English

The base index of the renamed realizer equals the target type; (F.ofEquiv E).σ = τ.

Русский

Базовый индекс переименованного реализатора равен целевой множестве: (F.ofEquiv E).σ = τ.

LaTeX

$$$(F.ofEquiv E).\\sigma = \\tau$.$$

Lean4

@[simp]
theorem ofEquiv_σ {f : Filter α} (F : f.Realizer) (E : F.σ ≃ τ) : (F.ofEquiv E).σ = τ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru