copy_eq

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.copy_eq

English

If S is a collection of sets and for all s ∈ S we have s ∈ f iff s ∈ g, then f = g.

Русский

Если для каждой множества s ∈ S выполняется s ∈ f ⇔ s ∈ g, то f = g.

LaTeX

$$$\forall s, (s \in S \iff s \in f) \Rightarrow f.copy S h = g$$$

Lean4

theorem copy_eq {S} (hmem : ∀ s, s ∈ S ↔ s ∈ f) : f.copy S hmem = f :=
  Filter.ext hmem

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

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

Разделы

Аффилиация

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