mono — Mathlib

English

If f.IsSubordinate U and U ⊆ V pointwise, then f.IsSubordinate V.

Русский

Если f подчинено U и U_i ⊆ V_i для каждого i, то f подчинено V.

LaTeX

$$$$ f.IsSubordinate(U) \rightarrow (\forall i, U_i \subseteq V_i) \rightarrow f.IsSubordinate(V). $$$$

Lean4

theorem mono {f : BumpCovering ι X s} {U V : ι → Set X} (hU : f.IsSubordinate U) (hV : ∀ i, U i ⊆ V i) :
    f.IsSubordinate V := fun i => Subset.trans (hU i) (hV i)

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