instTransSetMemSubset

Mathlib.Order.Filter.Basic

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

English

The same monotonicity principle for membership under subset relation.

Русский

Та же принцип монотонности для принадлежности относительно подмножества.

LaTeX

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

Lean4

instance : Trans Membership.mem (· ⊆ ·) (Membership.mem : Filter α → Set α → Prop) where
  trans h₁ h₂ := mem_of_superset h₁ h₂

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

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

Разделы

Аффилиация

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