mem_of_superset

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#Filter.HasBasis.mem_of_superset

English

If there exists i with p i and s i ⊆ t, then t ∈ l.

Русский

Если существует i такое, что p i и s i ⊆ t, то t ∈ l.

LaTeX

$$$p(i) \wedge s(i) \subseteq t \Rightarrow t \in l$$$

Lean4

protected theorem mem_of_superset (hl : l.HasBasis p s) (hi : p i) (ht : s i ⊆ t) : t ∈ l :=
  hl.mem_iff.2 ⟨i, hi, ht⟩

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

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

Разделы

Аффилиация

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