filter_inj — Mathlib

English

Two filtered finsets s.filter p and t.filter p are equal if and only if every element a with p a is in s exactly when it is in t.

Русский

Два отфильтрованных финсетa равны тогда и только тогда, когда каждый элемент, удовлетворяющий p, принадлежит s тогда же, когда принадлежит t.

LaTeX

$$s.filter p = t.filter p \\iff \\forall a, p a \\to (a \\in s \\iff a \\in t)$$

Lean4

theorem filter_inj : s.filter p = t.filter p ↔ ∀ ⦃a⦄, p a → (a ∈ s ↔ a ∈ t) := by simp [Finset.ext_iff]

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