zeroOfFactMem — Mathlib

English

If X is a pointed set with zero and s ⊆ X contains 0, then the subtype s has a distinguished zero given by (0, proof that 0 ∈ s).

Русский

Пусть X — множество с точкой нуля и s ⊆ X содержит 0. Тогда подпространство s (в виде подпочти X) имеет выделенный нулевой элемент, равный паре (0, доказательство 0 ∈ s).

LaTeX

$$$\\text{Zero }s = \\langle 0, h \\rangle\\quad\\text{где } h: 0 \\in s$$$

Lean4

/-- not marked as an instance because it would be a bad one in general, but it can
be useful when working with `ContinuousMapZero` and the non-unital continuous
functional calculus. -/
def _root_.Set.zeroOfFactMem {X : Type*} [Zero X] (s : Set X) [Fact (0 ∈ s)] : Zero s where zero := ⟨0, Fact.out⟩

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