instTransSetSupersetMem

Mathlib.Order.Filter.Basic

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

English

If s ⊆ t and s ∈ f, then t ∈ f.

Русский

Если s ⊆ t и s ∈ f, то t ∈ f.

LaTeX

$$$s \subseteq t \land s \in f \Rightarrow t \in f$$$

Lean4

instance : Trans (· ⊇ ·) ((· ∈ ·) : Set α → Filter α → Prop) (· ∈ ·) where trans h₁ h₂ := mem_of_superset h₂ h₁

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

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

Разделы

Аффилиация

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