eq_of_same_basis

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#Filter.HasBasis.eq_of_same_basis

English

If hl and hl' are HasBasis with the same p and s, then l = l'.

Русский

Если hl и hl' имеют одинаковый базис, то фильтры совпадают.

LaTeX

$$$(hl : l.HasBasis p s) \to (hl' : l'.HasBasis p s) \to l = l'$$$

Lean4

theorem eq_of_same_basis (hl : l.HasBasis p s) (hl' : l'.HasBasis p s) : l = l' :=
  by
  ext t
  rw [hl.mem_iff, hl'.mem_iff]

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

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

Разделы

Аффилиация

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