sSup_iff — Mathlib

English

For a set S of MorphismProperty on C and a morphism f, sSup S f holds exactly when there exists a W in S with W f.

Русский

Для множества свойств S над MorphismProperty и морфизма f верно: sSup S f ⇔ ∃ W ∈ S, W f.

LaTeX

$$$\\text{sSup}\\;S\\;f \\iff \\exists W \\in S, W(f).$$$

Lean4

@[simp]
theorem sSup_iff (S : Set (MorphismProperty C)) {X Y : C} (f : X ⟶ Y) : sSup S f ↔ ∃ (W : S), W.1 f :=
  by
  dsimp [sSup, iSup]
  constructor
  · rintro ⟨_, ⟨⟨_, ⟨⟨_, ⟨_, h⟩, rfl⟩, rfl⟩⟩, rfl⟩, hf⟩
    exact ⟨⟨_, h⟩, hf⟩
  · rintro ⟨⟨W, hW⟩, hf⟩
    exact ⟨_, ⟨⟨_, ⟨_, ⟨⟨W, hW⟩, rfl⟩⟩, rfl⟩, rfl⟩, hf⟩

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