mem_addGroupFilterBasis_iff — Mathlib

English

For V in the additive group filter basis generated by B, V is in the basis iff V equals some B_i.

Русский

Для V, принадлежащего базису фильтра по B, верно: V принадлежит базису тогда и только тогда, когда V = B_i для некоторого i.

LaTeX

$$$V \in hB.toRingFilterBasis.toAddGroupFilterBasis \iff \exists i, V = B i$$$

Lean4

theorem mem_addGroupFilterBasis_iff {V : Set A} : V ∈ hB.toRingFilterBasis.toAddGroupFilterBasis ↔ ∃ i, V = B i :=
  Iff.rfl

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