mem_finite_iff — Mathlib

English

For any object X in a category C, a presieve s on X belongs to the finite coverings if and only if its uncurry is a finite relation; i.e., the index set is finite.

Русский

Для любого объекта X в категории C простейшая прокладка s на X принадлежит к конечным покрытиям тогда и только тогда, когда её развёртка uncurry образует конечное отношение.

LaTeX

$$$s \in \operatorname{finite} C X \;\Longleftrightarrow\; s.uncurry.Finite$$$

Lean4

@[simp]
theorem mem_finite_iff {X : C} {s : Presieve X} : s ∈ finite C X ↔ s.uncurry.Finite :=
  Iff.rfl

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