proj_eq_of_subset — Mathlib

English

If ∀ i, J i → K i, then π(π C K) J = π C J.

Русский

Если ∀ i, J i → K i, то π(π C K) J = π C J.

LaTeX

$$$$ \\pi(\\pi C K) J = \\pi C J \\quad\\text{when } \\forall i, J(i) \\Rightarrow K(i).$$$$

Lean4

theorem proj_eq_of_subset (h : ∀ i, J i → K i) : π (π C K) J = π C J :=
  by
  ext x
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨y, ⟨z, hz, rfl⟩, rfl⟩ := h
    refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩
    rw [proj_comp_of_subset J K h]
  · obtain ⟨y, hy, rfl⟩ := h
    dsimp [π]
    rw [← Set.image_comp]
    refine ⟨y, hy, ?_⟩
    rw [proj_comp_of_subset J K h]

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