stableUnderComposition — Mathlib

English

Flat maps are closed under composition: if f and g are flat, then g ∘ f is flat.

Русский

Плоские отображения сохраняются под композицию: если f и g плоские, то g ∘ f плоское.

LaTeX

$$$$\text{StableUnderComposition}(Flat) \;:\; \text{if } f.flat, \; g.flat \Rightarrow (g\circ f).flat.$$$$

Lean4

theorem stableUnderComposition : StableUnderComposition Flat :=
  by
  introv R hf hg
  exact hf.comp hg

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