English
From a filter basis B on α × α, together with reflexivity, symmetry, and composition compatibility, build UniformSpace.Core α whose uniformity is B.filter and whose structure respects these properties.
Русский
Из базиса фильтров B на α×α с рефлексивностью, симметрией и совместимостью с композицией строим UniformSpace.Core α, чья равномерность равна B.filter и чьи структуры удовлетворяют этим свойствам.
LaTeX
$$$\\forall B : FilterBasis(\\alpha \\times \\alpha),\\; \\forall refl, symm, comp \\text{ satisfying the stated predicates},\\; UniformSpace.Core\\,\\alpha$$$
Lean4
/-- Defining a `UniformSpace.Core` from a filter basis satisfying some uniformity-like axioms. -/
def mkOfBasis {α : Type u} (B : FilterBasis (α × α)) (refl : ∀ r ∈ B, ∀ (x), (x, x) ∈ r)
(symm : ∀ r ∈ B, ∃ t ∈ B, t ⊆ Prod.swap ⁻¹' r) (comp : ∀ r ∈ B, ∃ t ∈ B, t ○ t ⊆ r) : UniformSpace.Core α
where
uniformity := B.filter
refl := B.hasBasis.ge_iff.mpr fun _r ru => idRel_subset.2 <| refl _ ru
symm := (B.hasBasis.tendsto_iff B.hasBasis).mpr symm
comp := (HasBasis.le_basis_iff (B.hasBasis.lift' (monotone_id.compRel monotone_id)) B.hasBasis).2 comp
