preimage — Mathlib

English

If s is a Sublattice and f is a lattice homomorphism, then the preimage f^{-1}(s) is a Sublattice.

Русский

Если s — субрешетка и f — однородная по структуре, то прообраз f^{-1}(s) — субрешетка.

LaTeX

$$IsSublattice s → IsSublattice (Set.preimage (inst_2.coe f) s)$$

Lean4

theorem preimage [FunLike F β α] [LatticeHomClass F β α] (hs : IsSublattice s) (f : F) : IsSublattice (f ⁻¹' s) :=
  ⟨hs.1.preimage _, hs.2.preimage _⟩

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