English
An alternative constructor for UniformSpace.Core from a filter basis B on α × α, provided with reflexivity, symmetry via swap, and composition axioms.
Русский
Альтернативный конструктор UniformSpace.Core из базиса фильтров B на α×α при условии рефлексивности, симметрии через обмен и аксиомы композиции.
LaTeX
$$$\\text{Let } B \\text{ be a filter basis on } \\alpha \\times \\alpha. \\\\text{If } B\\text{ satisfies reflexivity, symmetry, and composition, then }\\text{UniformSpace.Core }\\alpha\\text{ exists with }\\text{uniformity}=B.filter\\text{, refl, symm, comp as given.}$$$
Lean4
/-- An alternative constructor for `UniformSpace.Core`. This version unfolds various
`Filter`-related definitions. -/
def mk' {α : Type u} (U : Filter (α × α)) (refl : ∀ r ∈ U, ∀ (x), (x, x) ∈ r) (symm : ∀ r ∈ U, Prod.swap ⁻¹' r ∈ U)
(comp : ∀ r ∈ U, ∃ t ∈ U, t ○ t ⊆ r) : UniformSpace.Core α :=
⟨U, fun _r ru => idRel_subset.2 (refl _ ru), symm, fun _r ru =>
let ⟨_s, hs, hsr⟩ := comp _ ru
mem_of_superset (mem_lift' hs) hsr⟩
