mul_right

Mathlib.Topology.Algebra.FilterBasis

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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