mem_smul

Mathlib.Order.Filter.Pointwise

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

English

Membership equivalence for smul: t ∈ f • g iff ∃ t1 ∈ f, ∃ t2 ∈ g, t1 • t2 ⊆ t.

Русский

Членство в smul эквивалентно: ∃ t1 ∈ f, ∃ t2 ∈ g, t1 • t2 ⊆ t.

LaTeX

$$t ∈ f • g ↔ ∃ t1 ∈ f, ∃ t2 ∈ g, t1 • t2 ⊆ t$$

Lean4

@[to_additive]
theorem mem_smul : t ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t :=
  Iff.rfl

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

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

Разделы

Аффилиация

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