inf_arrow_factors_right — Mathlib

English

For a finite set s, and P, and i ∈ s, the component P(i) factors through the infimum arrow (s.inf P).arrow.

Русский

Для конечного множества s и P элемент i ∈ s факторизует стрелу (s.inf P).arrow через Pi.

LaTeX

$$$ (P i).Factors (s.inf P).arrow \\quad \\text{если } i \\in s $$$

Lean4

theorem inf_arrow_factors_right {B : C} (X Y : Subobject B) : Y.Factors (X ⊓ Y).arrow :=
  (factors_iff _ _).mpr ⟨ofLE (X ⊓ Y) Y (inf_le_right X Y), by simp⟩

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