inf_factors — Mathlib

English

(X ⊓ Y).Factors f ⇔ X.Factors f ∧ Y.Factors f.

Русский

(X ⊓ Y).Factors f эквивалентно X.Factors f и Y.Factors f.

LaTeX

$$$ (X \\cap Y).Factors f \\iff X.Factors f \\land Y.Factors f $$$

Lean4

@[simp]
theorem inf_factors {A B : C} {X Y : Subobject B} (f : A ⟶ B) : (X ⊓ Y).Factors f ↔ X.Factors f ∧ Y.Factors f :=
  ⟨fun h => ⟨factors_left_of_inf_factors h, factors_right_of_inf_factors h⟩,
    by
    revert X Y
    apply Quotient.ind₂'
    rintro X Y ⟨⟨g₁, rfl⟩, ⟨g₂, hg₂⟩⟩
    exact ⟨_, pullback.lift_snd_assoc _ _ hg₂ _⟩⟩

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