sup_objs_exists — Mathlib

English

Equivalence preserves filtered-or-empty property.

Русский

Эквивалентность сохраняет свойство фильтрованности или пустоты.

LaTeX

$$$IsFilteredOrEmpty(D)$ if $C ≃ D$ and $IsFilteredOrEmpty(C)$$$

Lean4

/-- Any finite collection of objects in a filtered category has an object "to the right".
-/
theorem sup_objs_exists (O : Finset C) : ∃ S : C, ∀ {X}, X ∈ O → Nonempty (X ⟶ S) := by
  classical
    induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsFiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use max X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨leftToMax _ _⟩
    · exact ⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩

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