fiber_subset_ofLE — Mathlib

English

If A ≤ B in DiscreteQuotient X and a ∈ A, then the fiber A.proj^{-1}({a}) is contained in B.proj^{-1}({ofLE h a}), where h is the order relation A' ≤ A used to compare quotients.

Русский

Пусть A ≤ B в DiscreteQuotient X и a ∈ A; тогда A.proj^{-1}({a}) ⊆ B.proj^{-1}({ofLE h a}), где h — дайлик отношение порядка между A' и A.

LaTeX

$$$A.\\mathrm{proj}^{-1}\\'\\{a\\} \\subseteq B.\\mathrm{proj}^{-1}\\'\\{\\mathrm{ofLE}\\ h\\ a\\}$$$

Lean4

theorem fiber_subset_ofLE {A B : DiscreteQuotient X} (h : A ≤ B) (a : A) : A.proj ⁻¹' { a } ⊆ B.proj ⁻¹' {ofLE h a} :=
  by
  rcases A.proj_surjective a with ⟨a, rfl⟩
  rw [fiber_eq, ofLE_proj, fiber_eq]
  exact fun _ h' => h h'

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