mem_pmap — Mathlib

English

Membership in the pmap of a filter along a partial function is equivalent to membership of the corresponding core set in the original filter.

Русский

Принадлежность элементa множеству в pmap равносильна принадлежности соответствующего ядра в исходный фильтр.

LaTeX

$$$ s \\in l.pmap f \\iff f.core s \\in l $$$

Lean4

@[simp]
theorem mem_pmap (f : α →. β) (l : Filter α) (s : Set β) : s ∈ l.pmap f ↔ f.core s ∈ l :=
  Iff.rfl

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