mul_left

Mathlib.Topology.Algebra.FilterBasis

URI: https://scilib.ai/kg/mathlib#RingFilterBasis.mul_left

English

For any x0 ∈ R and U ∈ BR there exists V ∈ BR with V ⊆ { x : R | x0 · x ∈ U }.

Русский

Для любого x0 ∈ R и U ∈ BR существует V ∈ BR, такой что V ⊆ { x ∈ R : x0 · x ∈ U }.

LaTeX

$$$\exists V\in BR, V \subseteq (\lambda x\, . x_0 * x)^{-1}' U$.$$

Lean4

theorem mul_left (x₀ : R) {U : Set R} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x) ⁻¹' U :=
  mul_left' x₀ hU

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

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

Разделы

Аффилиация

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