filter_inj' — Mathlib

English

Two filtered copies of the same finite set s with filters p and q are equal if and only if, for all a in s, p a ⇔ q a.

Русский

Две отфильтрованные копии одного и того же множества s с фильтрами p и q равны тогда и только тогда, когда для каждого элемента a ∈ s выполняется p a ⇔ q a.

LaTeX

$$s.filter p = s.filter q \\iff \\forall a \\in s, p a \\iff q a$$

Lean4

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

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