mp_mem

Mathlib.Order.Filter.Defs

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

English

If s ∈ f and the set {x | x ∈ s → x ∈ t} ∈ f, then t ∈ f.

Русский

Если s ∈ f и множество {x | x ∈ s → x ∈ t} ∈ f, то t ∈ f.

LaTeX

$$$\forall {f:\text{Filter}(\alpha)} {s t:Set\alpha}, s\in f \land \{x\mid x\in s\to x\in t\} \in f \Rightarrow t\in f$$$

Lean4

theorem mp_mem (hs : s ∈ f) (h : {x | x ∈ s → x ∈ t} ∈ f) : t ∈ f :=
  mem_of_superset (inter_mem hs h) fun _ ⟨h₁, h₂⟩ => h₂ h₁

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

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

Разделы

Аффилиация

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