principal — Mathlib

English

A CFilter yields a Realizer of the generated Filter by taking σ as the index, with the base data F, and the obvious equality proof.

Русский

CFilter порождает реализатор с базой данных, используя σ как индекс и F как базовый функционал, с очевидным доказательством тождества.

LaTeX

$$$\\mathrm{toRealizer}(F):= \\langle \\sigma, F, rfl \\rangle$.$$

Lean4

/-- `Unit` is a realizer for the principal filter -/
protected def principal (s : Set α) : (principal s).Realizer :=
  ⟨Unit,
    { f := fun _ ↦ s
      pt := ()
      inf := fun _ _ ↦ ()
      inf_le_left := fun _ _ ↦ le_rfl
      inf_le_right := fun _ _ ↦ le_rfl }, filter_eq <| Set.ext fun _ ↦ ⟨fun ⟨_, s⟩ ↦ s, fun h ↦ ⟨(), h⟩⟩⟩

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