Theorems · Theorem · order theory

Function.Injective.completelyDistribLatticeMinimalAxioms

∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  CompletelyDistribLattice.MinimalAxioms β →
    ∀ (f : α → β),
      Function.Injective f →
        (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
          (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) → CompletelyDistribLattice.MinimalAxioms α

Pullback a CompletelyDistribLattice.MinimalAxioms along an injection.

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLatticeCompleteLattice