Mathlib references

Every Mathlib declaration referred to directly by this project’s own code, grouped by the module it comes from.

definition abbreviation theorem
legend

Algebra.BigOperators.Fin

theorem Fin.sum_univ_add.{u_2} {M : Type u_2} [AddCommMonoid M] {a b : ℕ} (f : Fin (a + b) → M) :
  ∑ i, f i = ∑ i, f (Fin.castAdd b i) + ∑ i, f (Fin.natAdd a i)

Used by: Component.parallel, Component.symmetry

theorem Fin.sum_univ_one.{u_2} {M : Type u_2} [AddCommMonoid M] (f : Fin 1 → M) : ∑ i, f i = f 0

Used by: Component.Simplex.toInformationSystem, InformationSystem.toSimplex

theorem Fin.sum_univ_two.{u_2} {M : Type u_2} [AddCommMonoid M] (f : Fin 2 → M) : ∑ i, f i = f 0 + f 1

Used by: InformationSystem.parallel_delta

Algebra.BigOperators.Group.Finset.Basic

theorem Finset.sum_congr.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M]
  {f g : ι → M} (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g

Used by: Component.empty, Component.id, Component.parallel, Component.symmetry, Discrete.pi, Receiver.step, Sender.step

theorem Finset.sum_const.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (b : M) :
  ∑ _x ∈ s, b = s.card • b

Used by: Receiver.step, Sender.step

Algebra.BigOperators.Group.Finset.Defs

∑ x ∈ s, f x is the sum of f x as x ranges over the elements of the finite set s.

When the index type is a Fintype, the notation ∑ x, f x, is a shorthand for ∑ x ∈ Finset.univ, f x.

def Finset.sum.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : M

Used by: Component.Simplex.toInformationSystem, Component.id, Component.parallel, Component.symmetry, Discrete.pi, InformationSystem.parallel_delta, InformationSystem.toSimplex, Receiver.step, Sender.step, instNormForallFin_computerNetworks, instNormValue

Algebra.BigOperators.Ring.Finset

theorem Nat.cast_sum.{u_4, u_5} {R : Type u_4} {ι : Type u_5} [AddCommMonoidWithOne R] (s : Finset ι)
  (f : ι → ℕ) : ↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)

Used by: Discrete.pi

Algebra.CharP.Defs

theorem CharP.cast_eq_zero.{u_1} (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] : ↑p = 0

Used by: Frame.toPoly_degree_lt

Algebra.CharP.Two

theorem CharTwo.add_self_eq_zero.{u_1} {R : Type u_1} [Semiring R] [CharP R 2] (x : R) : x + x = 0

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_one_add_one, Frame.toPoly_set_flip

Algebra.Group.Basic

theorem mul_pow.{u_4} {M : Type u_4} [CommMonoid M] (a b : M) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n

Used by: phoneNumberInformation_eq

theorem sub_add_sub_cancel.{u_3} {G : Type u_3} [AddGroup G] (a b c : G) : a - b + (b - c) = a - c

Used by: InformationSystem.sequential_delta

Algebra.Group.Defs

theorem mul_one.{u} {M : Type u} [MulOneClass M] (a : M) : a * 1 = a

Used by: Frame.eq_of_associated_gf2, Frame.toPoly_append, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any, Receiver.step, Sender.step

theorem one_mul.{u} {M : Type u} [MulOneClass M] (a : M) : 1 * a = a

Used by: Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any

theorem one_pow.{u_2} {M : Type u_2} [Monoid M] (n : ℕ) : 1 ^ n = 1

Used by: no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

theorem pow_add.{u_2} {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n

Used by: BitFunction.cardinality_output_growth

theorem pow_mul.{u_2} {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ (m * n) = (a ^ m) ^ n

Used by: BitFunction.cardinality, BitFunction.cardinality_input_growth

theorem pow_succ.{u_2} {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a

Used by: BitFunction.cardinality_input_growth, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

theorem pow_succ'.{u_2} {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : a ^ (n + 1) = a * a ^ n

Used by: Frame.crcStep_poly

theorem pow_zero.{u_2} {M : Type u_2} [Monoid M] (a : M) : a ^ 0 = 1

Used by: Frame.crc_poly_dvd, Frame.toPoly_append, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

theorem sub_self.{u_1} {G : Type u_1} [AddGroup G] (a : G) : a - a = 0

Used by: InformationSystem.eval_delta

Algebra.Group.Hom.Defs

See note [hom simp lemma priority]

theorem map_one.{u_4, u_5, u_9} {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N]
  [OneHomClass F M N] (f : F) : f 1 = 1

Used by: Frame.eq_of_associated_gf2

Algebra.Group.Units.Defs

An element a : M of a Monoid is a unit if it has a two-sided inverse. The actual definition says that a is equal to some u : Mˣ, where Mˣ is a bundled version of IsUnit.

def IsUnit.{u_1} {M : Type u_1} [Monoid M] (a : M) : Prop

Used by: Frame.eq_of_associated_gf2

Units of a Monoid, bundled version. Notation: αˣ.

An element of a Monoid is a unit if it has a two-sided inverse. This version bundles the inverse element so that it can be computed. For a predicate see IsUnit.

structure Units.{u} (α : Type u) [Monoid α] : Type u

Used by: Frame.eq_of_associated_gf2

theorem Units.isUnit.{u_1} {M : Type u_1} [Monoid M] (u : Mˣ) : IsUnit ↑u

Used by: Frame.eq_of_associated_gf2

Algebra.GroupWithZero.Associated

Two elements of a Monoid are Associated if one of them is another one multiplied by a unit on the right.

def Associated.{u_1} {M : Type u_1} [Monoid M] (x y : M) : Prop

Used by: Frame.eq_of_associated_gf2, Frame.generator_not_dvd_pow

theorem dvd_prime_pow.{u_1} {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p q : M}
  (hp : Prime p) (n : ℕ) : q ∣ p ^ n ↔ ∃ i ≤ n, Associated q (p ^ i)

Used by: Frame.generator_not_dvd_pow

Algebra.GroupWithZero.Units.Basic

theorem IsUnit.ne_zero.{u_2} {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] {a : M₀} (ha : IsUnit a) :
  a ≠ 0

Used by: Frame.eq_of_associated_gf2

theorem div_eq_iff.{u_3} {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
  a / b = c ↔ a = c * b

Used by: irrational_logb_two_five, irrational_logb_two_three

Algebra.Order.BigOperators.Group.Finset

theorem Finset.sum_nonneg.{u_1, u_5} {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [Preorder N]
  {f : ι → N} {s : Finset ι} [AddLeftMono N] (h : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∑ i ∈ s, f i

Used by: instNormNonnegForallFin

Algebra.Order.GroupWithZero.Basic

theorem pow_pos.{u_2} {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀]
  [ZeroLEOneClass M₀] (ha : 0 < a) (n : ℕ) : 0 < a ^ n

Used by: phoneNumberInformation_eq

Algebra.Order.Monoid.Unbundled.Basic

Alias of Left.add_nonneg.

theorem add_nonneg.{u_1} {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a b : α} (ha : 0 ≤ a)
  (hb : 0 ≤ b) : 0 ≤ a + b

Used by: instNormNonnegProd

Algebra.Order.Ring.Unbundled.Rat

theorem Rat.num_pos {a : ℚ} : 0 < a.num ↔ 0 < a

Used by: irrational_logb_two_five, irrational_logb_two_three

Algebra.Order.Sub.Basic

theorem tsub_self.{u_1} {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α]
  [OrderedSub α] (a : α) : a - a = 0

Used by: Frame.crc32Ethernet_detects_single_bit_flip

Algebra.Order.Sub.Defs

theorem add_tsub_cancel_left.{u_1} {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α]
  [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a + b - a = b

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow

theorem tsub_zero.{u_1} {α : Type u_1} [PartialOrder α] [AddCommMonoid α] [Sub α] [OrderedSub α] (a : α) :
  a - 0 = a

Used by: Frame.crc32Ethernet_detects_single_bit_flip

Algebra.Polynomial.Basic

Polynomial R is the type of univariate polynomials over R, denoted as R[X] within the Polynomial namespace.

Polynomials should be seen as (semi-)rings with the additional constructor X. The embedding from R is called C.

structure Polynomial.{u_1} (R : Type u_1) [Semiring R] : Type u_1

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.eq_of_associated_gf2, Frame.generator_not_dvd_pow, Frame.toPoly, Frame.toPoly_append, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any, Frame.toPoly_one_add_one, Frame.toPoly_replicate_false, Frame.toPoly_set_flip, Frame.toPoly_xor

C a is the constant polynomial a. C is provided as a ring homomorphism.

def Polynomial.C.{u} {R : Type u} [Semiring R] : R →+* Polynomial R

Used by: Frame.eq_of_associated_gf2

Algebra.Polynomial.Degree.Defs

degree p is the degree of the polynomial p, i.e. the largest X-exponent in p. degree p = some n when p ≠ 0 and n is the highest power of X that appears in p, otherwise degree 0 = ⊥.

def Polynomial.degree.{u} {R : Type u} [Semiring R] (p : Polynomial R) : WithBot ℕ

Used by: Frame.generator_not_dvd_pow, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any

theorem Polynomial.degree_X.{u} {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.degree = 1

Used by: Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any

theorem Polynomial.degree_X_pow.{u} {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) :
  (Polynomial.X ^ n).degree = ↑n

Used by: Frame.generator_not_dvd_pow

theorem Polynomial.degree_add_le.{u} {R : Type u} [Semiring R] (p q : Polynomial R) :
  (p + q).degree ≤ max p.degree q.degree

Used by: Frame.toPoly_degree_lt

theorem Polynomial.degree_neg.{u} {R : Type u} [Ring R] (p : Polynomial R) : (-p).degree = p.degree

Used by: Frame.toPoly_ne_zero_of_any

Algebra.Polynomial.Degree.Operations

theorem Polynomial.degree_add_eq_left_of_degree_lt.{u} {R : Type u} [Semiring R] {p q : Polynomial R}
  (h : q.degree < p.degree) : (p + q).degree = p.degree

Used by: Frame.generator_not_dvd_pow

theorem Polynomial.degree_pow.{u} {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R]
  (p : Polynomial R) (n : ℕ) : (p ^ n).degree = n • p.degree

Used by: Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any

Algebra.Polynomial.Degree.Units

Characterization of a unit of a polynomial ring over an integral domain R. See Polynomial.isUnit_iff_coeff_isUnit_isNilpotent when R is a commutative ring.

theorem Polynomial.isUnit_iff.{u} {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} :
  IsUnit p ↔ ∃ r, IsUnit r ∧ Polynomial.C r = p

Used by: Frame.eq_of_associated_gf2

Algebra.Polynomial.RingDivision

theorem Polynomial.prime_X.{u} {R : Type u} [CommRing R] [IsDomain R] : Prime Polynomial.X

Used by: Frame.generator_not_dvd_pow

Algebra.Ring.Defs

theorem add_one_mul.{u} {α : Type u} [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
  (a + 1) * b = a * b + b

Used by: BitFunction.cardinality_output_growth

theorem nsmul_eq_mul.{u} {α : Type u} [NonAssocSemiring α] (n : ℕ) (a : α) : n • a = ↑n * a

Used by: Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any, Receiver.step, Sender.step

Algebra.Ring.Divisibility.Basic

theorem dvd_add.{u_1} {α : Type u_1} [Add α] [Semigroup α] [LeftDistribClass α] {a b c : α} (h₁ : a ∣ b)
  (h₂ : a ∣ c) : a ∣ b + c

Used by: Frame.crcFrom_detects_single_bit_flip

Algebra.Ring.Hom.Defs

Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both MonoidHom and MonoidWithZeroHom in order to put the fields in a sensible order, even though MonoidWithZeroHom already extends MonoidHom.

structure RingHom.{u_5, u_6} (α : Type u_5) (β : Type u_6) [NonAssocSemiring α] [NonAssocSemiring β] :
  Type (max u_5 u_6)

Used by: Frame.eq_of_associated_gf2

Algebra.Ring.Rat

theorem Rat.num_div_den (r : ℚ) : ↑r.num / ↑r.den = r

Used by: irrational_logb_two_five, irrational_logb_two_three

Analysis.Normed.Group.Defs

Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ‖x‖. This class is designed to be extended in more interesting classes specifying the properties of the norm.

structure Norm.{u_8} (E : Type u_8) : Type u_8

Used by: ApplicationLayer.interface, Channel, Channel.capacity, Channel.loss, Channel.lossless, Channel.lossless_stationary, Channel.lossy_loses_overall, Channel.maxWireSize, Channel.overall_loss, Channel.system, Component, Component.Arrow, Component.Arrow.Equiv, Component.Arrow.setoid, Component.Demultiplex, Component.Hom, Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_eqToHom, Component.Hom.comp_id, Component.Hom.eqToHom_comp, Component.Hom.eqToHom_eq_recast_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.recast, Component.Hom.recast_eqToHom, Component.Hom.recast_recast, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensor, Component.Hom.tensorUnit, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.Multiplex, Component.PROP, Component.Simplex, Component.Simplex.toInformationSystem, Component.braidedCategory, Component.braiding, Component.braiding_naturality_left, Component.braiding_naturality_right, Component.category, Component.empty, Component.empty_parallel, Component.equivalent_of_stationary, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id, Component.id_sequential, Component.interchange, Component.monoidalCategory, Component.monoidalCategoryStruct, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast, Component.recast_congr, Component.recast_parallel_left, Component.recast_parallel_right, Component.recast_recast, Component.sequential, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry, Component.symmetry_symmetry, DataLinkLayer.network, Discrete, Discrete.pi, Discrete.prod, Discrete.size, Discrete.size_eq, InformationSystem, InformationSystem.Chain, InformationSystem.Chain.length, InformationSystem.Chain.ofIsChain, InformationSystem.Environment, InformationSystem.Environment.ownState, InformationSystem.Environment.universe, InformationSystem.Environment.universe_isolated, InformationSystem.Run, InformationSystem.Run.cycle, InformationSystem.Run.final, InformationSystem.Run.initial, InformationSystem.Run.toChain, InformationSystem.Run.trajectory, InformationSystem.Run.trajectory_head, InformationSystem.Spontaneous, InformationSystem.Step, InformationSystem.Step.bottom, InformationSystem.Step.delta, InformationSystem.Step.delta_alt, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.delta, InformationSystem.equivalent, InformationSystem.equivalent_output, InformationSystem.equivalent_step, InformationSystem.eval, InformationSystem.eval_append, InformationSystem.eval_delta, InformationSystem.eval_trichotomy, InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InformationSystem.irreversible, InformationSystem.isolated, InformationSystem.natural, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.parallel, InformationSystem.parallel_delta, InformationSystem.perpetuous, InformationSystem.perpetuous_coherent, InformationSystem.reversible, InformationSystem.roundtrip_neutral, InformationSystem.sequential, InformationSystem.sequential_delta, InformationSystem.spontaneous, InformationSystem.spontaneous_no_self_return, InformationSystem.spontaneous_not_perpetuous, InformationSystem.stepAt, InformationSystem.toSimplex, InformationSystem.zero_run_le, InterfaceOld, InterfaceOld.Value.observe, InterfaceOld.homogeneous, InterfaceOld.single, InterfaceOld.tensor, InterfaceOld.unit, List.totalSize, NetworkArchitecture, NetworkArchitecture.application, NetworkArchitecture.dataLink, NetworkArchitecture.network, NetworkArchitecture.physical, NetworkArchitecture.stack, NetworkArchitecture.transport, NetworkLayer.forwards, NetworkLayer.interface, NetworkLayer.resolves, NetworkLayer.transport, NormNonneg, TransportLayer.application, TransportLayer.interface, instBraidedCategoryPROP, instCategoryPROP, instMonoidalCategoryPROP, instNormBit, instNormBool_computerNetworks, instNormCell, instNormEvent, instNormForallFin_computerNetworks, instNormFrame, instNormIcmp, instNormNonnegForallFin, instNormNonnegProd, instNormPacket, instNormProd_computerNetworks, instNormProtocol, instNormSegment, instNormSetBlock, instNormSignal, instNormUnit_computerNetworks, instNormValue

Analysis.SpecialFunctions.Log.Base

The real logarithm in a given base. As with the natural logarithm, we define logb b x to be logb b |x| for x < 0, and 0 for x = 0.

def Real.logb (b x : ℝ) : ℝ

Used by: irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, irrational_trafficLightInformation, phoneNumberInformation, phoneNumberInformation_eq, trafficLightInformation, trafficLightInformation_eq

theorem Real.logb_mul {b x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :
  Real.logb b (x * y) = Real.logb b x + Real.logb b y

Used by: phoneNumberInformation_eq

theorem Real.logb_pow (b x : ℝ) (k : ℕ) : Real.logb b (x ^ k) = ↑k * Real.logb b x

Used by: phoneNumberInformation_eq

theorem Real.logb_self_eq_one {b : ℝ} (hb : 1 < b) : Real.logb b b = 1

Used by: phoneNumberInformation_eq

theorem Real.rpow_logb {b x : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) (hx : 0 < x) : b ^ Real.logb b x = x

Used by: irrational_logb_two_five, irrational_logb_two_three

Analysis.SpecialFunctions.Pow.Real

theorem Real.rpow_lt_rpow_left_iff {x y z : ℝ} (hx : 1 < x) : x ^ y < x ^ z ↔ y < z

Used by: irrational_logb_two_five, irrational_logb_two_three

theorem Real.rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z

Used by: irrational_logb_two_five, irrational_logb_two_three

theorem Real.rpow_natCast (x : ℝ) (n : ℕ) : x ^ ↑n = x ^ n

Used by: irrational_logb_two_five, irrational_logb_two_three

theorem Real.rpow_zero (x : ℝ) : x ^ 0 = 1

Used by: irrational_logb_two_five, irrational_logb_two_three

CategoryTheory.Adjunction.Basic

F ⊣ G represents the data of an adjunction between two functors F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.

We use the unit-counit definition of an adjunction. There is a constructor Adjunction.mk' which constructs an adjunction from the data of a hom set equivalence, a unit, and a counit, together with proofs of the equalities homEquiv_unit and homEquiv_counit relating them to each other.

There is also a constructor Adjunction.mkOfHomEquiv which constructs an adjunction from a natural hom set equivalence.

To construct adjoints to a given functor, there are constructors leftAdjointOfEquiv and adjunctionOfEquivLeft (as well as their duals).

structure CategoryTheory.Adjunction.{v₁, v₂, u₁, u₂} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C]
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D C) : Type (max (max (max u₁ u₂) v₁) v₂)

Used by: Specification.closed

CategoryTheory.Category.Basic

The typeclass Category C describes morphisms associated to objects of type C. The universe levels of the objects and morphisms are unconstrained, and will often need to be specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.)

structure CategoryTheory.Category.{v, u} (obj : Type u) : Type (max u (v + 1))

Used by: Component.category, Specification.category, instCategoryPROP

CategoryTheory.Category.Cat

Category of categories.

def CategoryTheory.Cat.{v, u} : Type (max (u + 1) u (v + 1))

Used by: Topology.joinFunctor, Topology.joinHistory, Topology.runArrows, Topology.runArrows'

Construct a bundled Cat from the underlying type and the typeclass.

def CategoryTheory.Cat.of.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Cat

Used by: Topology.joinHistory, Topology.runArrows, Topology.runArrows'

The 1-morphism in Cat corresponding to a functor.

def CategoryTheory.Functor.toCatHom.{v, u} {C D : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) :
  CategoryTheory.Cat.of C ⟶ CategoryTheory.Cat.of D

Used by: Topology.joinFunctor, Topology.runArrows'

CategoryTheory.Category.GaloisConnection

A Galois connection between preorders induces an adjunction between the associated categories.

def GaloisConnection.adjunction.{u, v} {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {l : X → Y}
  {u : Y → X} (gc : GaloisConnection l u) : ⋯.functor ⊣ ⋯.functor

Used by: Specification.closed

CategoryTheory.Category.Preorder

Express an inequality as a morphism in the corresponding preorder category.

def CategoryTheory.homOfLE.{u} {X : Type u} [Preorder X] {x y : X} (h : x ≤ y) : x ⟶ y

Used by: Specification.binaryCone, Topology.IsNerveCover, Topology.isNerveCover_inter, Topology.nerveCoverage, Topology.restrictPresieve

Extract the underlying inequality from a morphism in a preorder category.

theorem CategoryTheory.leOfHom.{u} {X : Type u} [Preorder X] {x y : X} (h : x ⟶ y) : x ≤ y

Used by: Topology.isNerveCover_inter, Topology.joinFunctor

A monotone function between preorders induces a functor between the associated categories.

def Monotone.functor.{u, v} {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {f : X → Y}
  (h : Monotone f) : CategoryTheory.Functor X Y

Used by: Specification.closed, Topology.joinCoverage, Topology.leaveCoverage

CategoryTheory.ComposableArrows.Basic

ComposableArrows C n is the type of functors Fin (n + 1) ⥤ C.

abbrev CategoryTheory.ComposableArrows.{v_1, u_1} (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C]
  (n : ℕ) : Type (max v_1 u_1)

Used by: Topology.runArrows, Topology.runArrows'

The leftmost object of F : ComposableArrows C n.

abbrev CategoryTheory.ComposableArrows.left.{v_1, u_1} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) : C

Used by: Topology.runArrows, Topology.runArrows'

Constructor for ComposableArrows C 0.

def CategoryTheory.ComposableArrows.mk₀.{v_1, u_1} {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C]
  (X : C) : CategoryTheory.ComposableArrows C 0

Used by: Topology.runArrows'

“Precomposition” of F : ComposableArrows C n by a morphism f : X ⟶ F.left.

def CategoryTheory.ComposableArrows.precomp.{v_1, u_1} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) : CategoryTheory.ComposableArrows C (n + 1)

Used by: Topology.runArrows'

CategoryTheory.Discrete.Basic

A wrapper for promoting any type to a category, with the only morphisms being equalities.

structure CategoryTheory.Discrete.{u₁} (α : Type u₁) : Type u₁

Used by: Specification.binaryCone, Specification.terminalCone

CategoryTheory.EqToHom

Proving equality between functors. This isn’t an extensionality lemma, because usually you don’t really want to do this.

theorem CategoryTheory.Functor.ext.{v₁, v₂, u₁, u₂} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C]
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D}
  (h_obj : ∀ (X : C), F.obj X = G.obj X)
  (h_map :
    ∀ (X Y : C) (f : X ⟶ Y),
      F.map f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯)) := by
    cat_disch) :
  F = G

Used by: Specification.closed

Reducible form of congrArg_mpr_hom_left

theorem CategoryTheory.congrArg_cast_hom_left.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C]
  {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
  cast ⋯ q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q

Used by: Specification.terminalCone

An equality X = Y gives us a morphism X ⟶ Y.

It is typically better to use this, rather than rewriting by the equality then using 1 _ which usually leads to dependent type theory hell.

def CategoryTheory.eqToHom.{v₁, u₁} {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : X ⟶ Y

Used by: Component.Hom.comp_eqToHom, Component.Hom.eqToHom_comp, Component.Hom.eqToHom_eq_recast_id, Component.Hom.recast_eqToHom, Component.braidedCategory, Component.monoidalCategory, Specification.closed, Specification.terminalCone

An equality X = Y gives us an isomorphism X ≅ Y.

It is typically better to use this, rather than rewriting by the equality then using Iso.refl _ which usually leads to dependent type theory hell.

def CategoryTheory.eqToIso.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : X ≅ Y

Used by: Component.braidedCategory, Component.monoidalCategory, Component.monoidalCategoryStruct

theorem CategoryTheory.eqToIso.hom.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : (CategoryTheory.eqToIso p).hom = CategoryTheory.eqToHom p

Used by: Component.braidedCategory, Component.monoidalCategory

theorem CategoryTheory.eqToIso.inv.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : (CategoryTheory.eqToIso p).inv = CategoryTheory.eqToHom ⋯

Used by: Component.braidedCategory

CategoryTheory.Functor.Basic

Functor C D represents a functor between categories C and D.

To apply a functor F to an object use F.obj X, and to a morphism use F.map f.

The axiom map_id expresses preservation of identities, and map_comp expresses functoriality.

structure CategoryTheory.Functor.{v₁, v₂, u₁, u₂} (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C]
  (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : Type (max v₁ v₂ u₁ u₂)

Used by: Specification.closed, Specification.terminalCone, Topology.Step.coverageFunctor, Topology.joinCoverage, Topology.joinFunctor, Topology.leaveCoverage

1 C is the identity functor on a category C.

def CategoryTheory.Functor.id.{v₁, u₁} (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
  CategoryTheory.Functor C C

Used by: Topology.Step.coverageFunctor, Topology.joinFunctor

CategoryTheory.Functor.Const

The functor sending X : C to the constant functor J ⥤ C sending everything to X.

def CategoryTheory.Functor.const.{v₁, v₂, u₁, u₂} (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J]
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] :
  CategoryTheory.Functor C (CategoryTheory.Functor J C)

Used by: Specification.terminalCone

theorem CategoryTheory.Functor.const_obj_map.{v₁, v₂, u₁, u₂} (J : Type u₁)
  [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C)
  {X✝ Y✝ : J} (x✝ : X✝ ⟶ Y✝) :
  ((CategoryTheory.Functor.const J).obj X).map x✝ = CategoryTheory.CategoryStruct.id X

Used by: Specification.terminalCone

theorem CategoryTheory.Functor.const_obj_obj.{v₁, v₂, u₁, u₂} (J : Type u₁)
  [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C)
  (x✝ : J) : ((CategoryTheory.Functor.const J).obj X).obj x✝ = X

Used by: Specification.terminalCone

CategoryTheory.Grothendieck

The Grothendieck construction (often written as ∫ F in mathematics) for a functor F : C ⥤ Cat gives a category whose * objects X consist of X.base : C and X.fiber : F.obj base * morphisms f : X ⟶ Y consist of base : X.base ⟶ Y.base and f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber

structure CategoryTheory.Grothendieck.{u, v, u₂, v₂} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) : Type (max u u₂)

Used by: Topology.joinGrothendieck, Topology.runGrothendieck

CategoryTheory.Iso

An isomorphism (a.k.a. an invertible morphism) between two objects of a category. The inverse morphism is bundled.

See also CategoryTheory.Core for the category with the same objects and isomorphisms playing the role of morphisms.

structure CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type v

Used by: Component.braiding

Identity isomorphism.

def CategoryTheory.Iso.refl.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : X ≅ X

Used by: Specification.terminalCone

CategoryTheory.Limits.HasLimits

LimitCone F contains a cone over F together with the information that it is a limit.

structure CategoryTheory.Limits.LimitCone.{v₁, u₁, v, u} {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J]
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) :
  Type (max (max u u₁) v)

Used by: Specification.binaryCone, Specification.terminalCone

CategoryTheory.Limits.Preorder

The infimum of two elements in a preordered type is a binary product in the category associated to this preorder.

def Preorder.isLimitBinaryFan.{u} {C : Type u} [SemilatticeInf C] (X Y : C) :
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯))

Used by: Specification.binaryCone

If C is a preorder with top, then ⊤ is a terminal object.

def Preorder.isTerminalTop.{u} (C : Type u) [Preorder C] [OrderTop C] :
  CategoryTheory.Limits.IsTerminal ⊤

Used by: Specification.terminalCone

CategoryTheory.Limits.Shapes.BinaryProducts

A binary fan with vertex P consists of the two projections π₁ : P ⟶ X and π₂ : P ⟶ Y.

def CategoryTheory.Limits.BinaryFan.mk.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : CategoryTheory.Limits.BinaryFan X Y

Used by: Specification.binaryCone

The type of objects for the diagram indexing a binary (co)product.

inductive CategoryTheory.Limits.WalkingPair : Type

Used by: Specification.binaryCone

The diagram on the walking pair, sending the two points to X and Y.

def CategoryTheory.Limits.pair.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) :
  CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C

Used by: Specification.binaryCone

CategoryTheory.Limits.Shapes.IsTerminal

Construct a cone for the empty diagram given an object.

def CategoryTheory.Limits.asEmptyCone.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C]
  (X : C) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)

Used by: Specification.terminalCone

Being terminal is independent of the empty diagram, its universe, and the cone over it, as long as the cone points are isomorphic.

def CategoryTheory.Limits.isLimitChangeEmptyCone.{w, w', v₁, u₁} (C : Type u₁)
  [CategoryTheory.Category.{v₁, u₁} C]
  {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C}
  {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1}) C}
  {c₁ : CategoryTheory.Limits.Cone F₁} (hl : CategoryTheory.Limits.IsLimit c₁)
  (c₂ : CategoryTheory.Limits.Cone F₂) (hi : c₁.pt ≅ c₂.pt) : CategoryTheory.Limits.IsLimit c₂

Used by: Specification.terminalCone

CategoryTheory.Monoidal.Braided.Basic

A braided monoidal category is a monoidal category equipped with a braiding isomorphism β_ X Y : X ⊗ Y ≅ Y ⊗ X which is natural in both arguments, and also satisfies the two hexagon identities.

structure CategoryTheory.BraidedCategory.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] : Type (max u v)

Used by: Component.braidedCategory, instBraidedCategoryPROP

CategoryTheory.Monoidal.Cartesian.Basic

An instance of CartesianMonoidalCategory C bundles an explicit choice of a binary product of two objects of C, and a terminal object in C.

Users should use the monoidal notation: X ⊗ Y for the product and 1_ C for the terminal object.

structure CategoryTheory.CartesianMonoidalCategory.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C] :
  Type (max u v)

Used by: Specification.cartesianMonoidalCategory

Construct an instance of CartesianMonoidalCategory C given a terminal object and limit cones over arbitrary pairs of objects.

abbrev CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  (T : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C))
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) :
  CategoryTheory.CartesianMonoidalCategory C

Used by: Specification.cartesianMonoidalCategory

CategoryTheory.Monoidal.Category

In a monoidal category, we can take the tensor product of objects, X ⊗ Y and of morphisms f ⊗ₘ g. Tensor product does not need to be strictly associative on objects, but there is a specified associator, α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z). There is a tensor unit 1_ C, with specified left and right unitor isomorphisms λ_ X : 1_ C ⊗ X ≅ X and ρ_ X : X ⊗ 1_ C ≅ X. These associators and unitors satisfy the pentagon and triangle equations.

structure CategoryTheory.MonoidalCategory.{v, u} (C : Type u) [C : CategoryTheory.Category.{v, u} C] :
  Type (max u v)

Used by: Component.monoidalCategory, instMonoidalCategoryPROP

A constructor for monoidal categories that requires tensorHom instead of whiskerLeft and whiskerRight.

abbrev CategoryTheory.MonoidalCategory.ofTensorHom.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategoryStruct C]
  (id_tensorHom_id :
    ∀ (X₁ X₂ : C),
      CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₁)
          (CategoryTheory.CategoryStruct.id X₂) =
        CategoryTheory.CategoryStruct.id
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) := by
    cat_disch)
  (id_tensorHom :
    ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
      CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) f =
        CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f := by
    cat_disch)
  (tensorHom_id :
    ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
      CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Y) =
        CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y := by
    cat_disch)
  (tensorHom_comp_tensorHom :
    ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
        CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
          (CategoryTheory.CategoryStruct.comp f₂ g₂) := by
    cat_disch)
  (associator_naturality :
    ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
          (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁
            (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃)) := by
    cat_disch)
  (leftUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
            f)
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
          f := by
    cat_disch)
  (rightUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f
            (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
          f := by
    cat_disch)
  (pentagon :
    ∀ (W X Y Z : C),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
            (CategoryTheory.CategoryStruct.id Z))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.associator W
                (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
            (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
              (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator
              (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
          (CategoryTheory.MonoidalCategoryStruct.associator W X
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom := by
    cat_disch)
  (triangle :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator X
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
        CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
          (CategoryTheory.CategoryStruct.id Y) := by
    cat_disch) :
  CategoryTheory.MonoidalCategory C

Used by: Component.monoidalCategory

Tensoring on the left with a fixed object, as a functor.

abbrev CategoryTheory.MonoidalCategory.tensorLeft.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.Functor C C

Used by: Specification.closed

Auxiliary structure to carry only the data fields of (and provide notation for) MonoidalCategory.

structure CategoryTheory.MonoidalCategoryStruct.{v, u} (C : Type u) [C : CategoryTheory.Category.{v, u} C] :
  Type (max u v)

Used by: Component.monoidalCategoryStruct

CategoryTheory.Monoidal.Closed.Basic

An object X is (right) closed if (X ⊗ -) is a left adjoint.

structure CategoryTheory.Closed.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u v)

Used by: Specification.closed

A monoidal category C is (right) monoidal closed if every object is (right) closed.

structure CategoryTheory.MonoidalClosed.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] : Type (max u v)

Used by: Specification.monoidalClosed

CategoryTheory.PEmpty

The canonical functor out of the empty category.

def CategoryTheory.Functor.empty.{w, v, u} (C : Type u) [CategoryTheory.Category.{v, u} C] :
  CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C

Used by: Specification.terminalCone

CategoryTheory.Sites.Coverage

The type Coverage C of coverages on C. A coverage is a collection of covering presieves on every object X : C, which satisfies a pullback compatibility condition. Explicitly, this condition says that whenever S is a covering presieve for X and f : Y ⟶ X is a morphism, then there exists some covering presieve T for Y such that T factors through S along f.

structure CategoryTheory.Coverage.{v_1, u_1} (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] :
  Type (max u_1 v_1)

Used by: Topology.nerveCoverage

The Grothendieck topology associated to a coverage K. It is defined inductively as follows: 1. If S is a covering presieve for K, then the sieve generated by S is a covering sieve for the associated Grothendieck topology. 2. The top sieves are in the associated Grothendieck topology. 3. Add all sieves required by the local character axiom of a Grothendieck topology.

The pullback compatibility condition for a coverage ensures that the associated Grothendieck topology is pullback stable, and so an additional constructor in the inductive construction is not needed.

def CategoryTheory.Coverage.toGrothendieck.{v_1, u_1} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) :
  CategoryTheory.GrothendieckTopology C

Used by: Topology.nerveTopology

Given a morphism f : Y ⟶ X, a presieve S on Y and presieve T on X, we say that S factors through T along f, written S.FactorsThruAlong T f, provided that for any morphism g : Z ⟶ Y in S, there exists some morphism e : W ⟶ X in T and some morphism i : Z ⟶ W such that the obvious square commutes: i ≫ e = g ≫ f.

This is used in the definition of a coverage.

def CategoryTheory.Presieve.FactorsThruAlong.{v_1, u_1} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (S : CategoryTheory.Presieve Y)
  (T : CategoryTheory.Presieve X) (f : Y ⟶ X) : Prop

Used by: Topology.nerveCoverage

CategoryTheory.Sites.Grothendieck

The definition of a Grothendieck topology: a set of sieves J X on each object X satisfying three axioms: 1. For every object X, the maximal sieve is in J X. 2. If S ∈ J X then its pullback along any h : Y ⟶ X is in J Y. 3. If S ∈ J X and R is a sieve on X, then provided that the pullback of R along any arrow f : Y ⟶ X in S is in J Y, we have that R itself is in J X.

A sieve S on X is referred to as J-covering, (or just covering), if S ∈ J X.

See also [nlab] or [MM92] Chapter III, Section 2, Definition 1.

structure CategoryTheory.GrothendieckTopology.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C] :
  Type (max u v)

Used by: Heap.grothendieckTopology, Topology.nerveTopology, Tower.grothendieckTopology

CategoryTheory.Sites.Sieves

A predicate on arrows with codomain X.

def CategoryTheory.Presieve.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
  Type (max u₁ v₁)

Used by: Topology.IsNerveCover, Topology.isNerveCover_inter, Topology.nerveCoverage, Topology.restrictPresieve

CategoryTheory.Sites.Spaces

The Grothendieck topology associated to a topological space.

def Opens.grothendieckTopology.{u} (T : Type u) [TopologicalSpace T] :
  CategoryTheory.GrothendieckTopology (TopologicalSpace.Opens T)

Used by: Heap.grothendieckTopology

Combinatorics.SimpleGraph.Acyclic

The graph resulting from removing a vertex of degree one from a connected graph is connected.

theorem SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one.{u_1} {V : Type u_1}
  {G : SimpleGraph V} (hconn : G.Connected) {v : V} [Fintype ↑(G.neighborSet v)]
  (hdeg : G.degree v = 1) : (SimpleGraph.induce {v}ᶜ G).Connected

Used by: Topology.leave_preserves_connected

Combinatorics.SimpleGraph.Basic

A simple graph is an irreflexive symmetric relation Adj on a vertex type V. The relation describes which pairs of vertices are adjacent. There is exactly one edge for every pair of adjacent vertices; see SimpleGraph.edgeSet for the corresponding edge set.

structure SimpleGraph.{u} (V : Type u) : Type u

Used by: SimpleGraph.induceComplSingletonEquiv, Topology, Topology.whole, Topology.whole_adj_of_internal, Topology.whole_adj_of_link

Construct the simple graph induced by the given relation. It symmetrizes the relation and makes it irreflexive.

def SimpleGraph.fromRel.{u} {V : Type u} (r : V → V → Prop) : SimpleGraph V

Used by: Topology.whole, Topology.whole_adj_of_internal, Topology.whole_adj_of_link

theorem SimpleGraph.fromRel_adj.{u} {V : Type u} (r : V → V → Prop) (v w : V) :
  (SimpleGraph.fromRel r).Adj v w ↔ v ≠ w ∧ (r v w ∨ r w v)

Used by: Topology.whole_adj_of_internal, Topology.whole_adj_of_link

theorem SimpleGraph.ne_of_adj.{u} {V : Type u} (G : SimpleGraph V) {a b : V} (h : G.Adj a b) : a ≠ b

Used by: Topology.whole_adj_of_internal, Topology.whole_adj_of_link

G.neighborSet v is the set of vertices adjacent to v in G.

def SimpleGraph.neighborSet.{u} {V : Type u} (G : SimpleGraph V) (v : V) : Set V

Used by: Topology.leave_preserves_connected

Combinatorics.SimpleGraph.Connectivity.Connected

A graph is connected if it’s preconnected and contains at least one vertex. This follows the convention observed by mathlib that something is connected iff it has exactly one connected component.

There is a CoeFun instance so that h u v can be used instead of h.Preconnected u v.

structure SimpleGraph.Connected.{u} {V : Type u} (G : SimpleGraph V) : Prop

Used by: Topology.join_preserves_connected, Topology.leave_preserves_connected, Topology.whole_connected, Topology.whole_reachable_of_external

theorem SimpleGraph.Iso.connected_iff.{u, v} {V : Type u} {V' : Type v} {G : SimpleGraph V}
  {H : SimpleGraph V'} (e : G ≃g H) : G.Connected ↔ H.Connected

Used by: Topology.leave_preserves_connected

Two vertices are reachable if there is a walk between them. This is equivalent to Relation.ReflTransGen of G.Adj. See SimpleGraph.reachable_iff_reflTransGen.

def SimpleGraph.Reachable.{u} {V : Type u} (G : SimpleGraph V) (u v : V) : Prop

Used by: Topology.whole_reachable_of_external, Topology.whole_reachable_of_internal

theorem SimpleGraph.Reachable.refl.{u} {V : Type u} {G : SimpleGraph V} (u : V) : G.Reachable u u

Used by: Topology.whole_reachable_of_internal

theorem SimpleGraph.Reachable.trans.{u} {V : Type u} {G : SimpleGraph V} {u v w : V} (huv : G.Reachable u v)
  (hvw : G.Reachable v w) : G.Reachable u w

Used by: Topology.whole_reachable_of_external, Topology.whole_reachable_of_internal

Combinatorics.SimpleGraph.Connectivity.Subgraph

theorem SimpleGraph.induce_pair_connected_of_adj.{u} {V : Type u} {G : SimpleGraph V} {u v : V}
  (huv : G.Adj u v) : (SimpleGraph.induce {u, v} G).Connected

Used by: Topology.join_preserves_connected

theorem SimpleGraph.induce_union_connected.{u} {V : Type u} {G : SimpleGraph V} {s t : Set V}
  (sconn : (SimpleGraph.induce s G).Preconnected) (tconn : (SimpleGraph.induce t G).Preconnected)
  (sintert : (s ∩ t).Nonempty) : (SimpleGraph.induce (s ∪ t) G).Connected

Used by: Topology.join_preserves_connected

Combinatorics.SimpleGraph.Finite

G.degree v is the number of vertices adjacent to v.

def SimpleGraph.degree.{u_1} {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ↑(G.neighborSet v)] : ℕ

Used by: Topology.leave_preserves_connected

Combinatorics.SimpleGraph.Maps

A graph isomorphism is a bijective map on vertex sets that respects adjacency relations.

The notation G ≃g G' represents the type of graph isomorphisms.

abbrev SimpleGraph.Iso.{u_1, u_2} {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) :
  Type (max u_1 u_2)

Used by: SimpleGraph.induceComplSingletonEquiv

Restrict a graph to the vertices in the set s, deleting all edges incident to vertices outside the set. This is a wrapper around SimpleGraph.comap.

abbrev SimpleGraph.induce.{u_1} {V : Type u_1} (s : Set V) (G : SimpleGraph V) : SimpleGraph ↑s

Used by: SimpleGraph.induceComplSingletonEquiv, Topology.IsNerveCover, Topology.isNerveCover_inter, Topology.join_preserves_connected, Topology.leave_preserves_connected, Topology.restrict

theorem SimpleGraph.induce_adj.{u_1} {V : Type u_1} {G : SimpleGraph V} {s : Set V} {u v : ↑s} :
  (SimpleGraph.induce s G).Adj u v ↔ G.Adj ↑u ↑v

Used by: Topology.restrict

Combinatorics.SimpleGraph.Walk.Basic

A walk is a sequence of adjacent vertices. For vertices u v : V, the type walk u v consists of all walks starting at u and ending at v.

We say that a walk visits the vertices it contains. The set of vertices a walk visits is SimpleGraph.Walk.support.

See SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons' for patterns that can be useful in definitions since they make the vertices explicit.

inductive SimpleGraph.Walk.{u} {V : Type u} (G : SimpleGraph V) : V → V → Type u

Used by: Topology.whole_reachable_of_external, Topology.whole_reachable_of_internal

Data.Fin.Basic

theorem Fin.cast_injective {k l : ℕ} (h : k = l) : Function.Injective (Fin.cast h)

Used by: arithStepNeg_injective, arithStepNeg_not_surjective

theorem Fin.val_one' (n : ℕ) [NeZero n] : ↑1 = 1 % n

Used by: Structure.Arithmetic.S_iff_add_one

Data.Fin.SuccPred

theorem Fin.castSucc_injective (n : ℕ) : Function.Injective Fin.castSucc

Used by: Structure.Arithmetic.finTower, arithStepNeg_injective, arithTower

Data.Fin.Tuple.Basic

Append a tuple of length m to a tuple of length n to get a tuple of length m + n. This is a non-dependent version of Fin.add_cases.

def Fin.append.{u_1} {m n : ℕ} {α : Sort u_1} (a : Fin m → α) (b : Fin n → α) : Fin (m + n) → α

Used by: Component.Hom.tensor_id_id, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.interchange, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.symmetry, Component.symmetry_symmetry, DataLinkLayer.physical, Fin.append_eval, InformationSystem.parallel_delta

theorem Fin.append_assoc.{u_1} {m n : ℕ} {α : Sort u_1} {p : ℕ} (a : Fin m → α) (b : Fin n → α)
  (c : Fin p → α) : Fin.append (Fin.append a b) c = Fin.append a (Fin.append b c) ∘ Fin.cast ⋯

Used by: Component.parallel_assoc

theorem Fin.append_castAdd_natAdd.{u_1} {m n : ℕ} {α : Sort u_1} {f : Fin (m + n) → α} :
  (Fin.append (fun i => f (Fin.castAdd n i)) fun i => f (Fin.natAdd m i)) = f

Used by: Component.Hom.tensor_id_id, Component.symmetry_symmetry

theorem Fin.append_elim0.{u_1} {m : ℕ} {α : Sort u_1} (u : Fin m → α) :
  Fin.append u Fin.elim0 = u ∘ Fin.cast ⋯

Used by: Component.parallel_empty

theorem Fin.append_left.{u_1} {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin m) :
  Fin.append u v (Fin.castAdd n i) = u i

Used by: Component.interchange, Component.parallel, Component.parallel_comm, Component.symmetry, Component.symmetry_symmetry, Fin.append_eval

theorem Fin.append_left_nil.{u_1} {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (hu : m = 0) :
  Fin.append u v = v ∘ Fin.cast ⋯

Used by: Component.empty_parallel

theorem Fin.append_right.{u_1} {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin n) :
  Fin.append u v (Fin.natAdd m i) = v i

Used by: Component.interchange, Component.parallel, Component.parallel_comm, Component.symmetry, Component.symmetry_symmetry, Fin.append_eval

Data.Fin.VecNotation

vecCons h t prepends an entry h to a vector t.

The inverse functions are vecHead and vecTail. The notation ![a, b, ...] expands to vecCons a (vecCons b ...).

def Matrix.vecCons.{u} {α : Type u} {n : ℕ} (h : α) (t : Fin n → α) : Fin n.succ → α

Used by: Tower, arithPlus_iff, arithPlus_succ, arithPlus_zero, arithSucc_functional, arithSucc_iff, arithSucc_iff_eq_succFun, arithSucc_no_fixed_point, arithSucc_total, arithTower, arithZero_not_succ, arithZero_unique

Data.Finite.Defs

A type is Finite if it is in bijective correspondence to some Fin n.

This is similar to Fintype, but Finite is a proposition rather than data. A particular benefit to this is that Finite instances are definitionally equal to one another (due to proof irrelevance) rather than being merely propositionally equal, and, furthermore, Finite instances generally avoid the need for Decidable instances. One other notable difference is that Finite allows there to be Finite p instances for all p : Prop, which is not allowed by Fintype due to universe constraints. An application of this is that Finite (x ∈ s → β x) follows from the general instance for pi types, assuming [∀ x, Finite (β x)]. Implementation note: this is a reason Finite α is not defined as Nonempty (Fintype α).

Every Fintype instance provides a Finite instance via Finite.of_fintype. Conversely, one can noncomputably create a Fintype instance from a Finite instance via Fintype.ofFinite. In a proof one might write

  have := Fintype.ofFinite α

to obtain such an instance.

Do not write noncomputable Fintype instances; instead write Finite instances and use this Fintype.ofFinite interface. The Fintype instances should be relied upon to be computable for evaluation purposes.

Theorems should use Finite instead of Fintype, unless definitions in the theorem statement require Fintype. Definitions should prefer Finite as well, unless it is important that the definitions are meant to be computable in the reduction or #eval sense.

inductive Finite.{u_3} (α : Sort u_3) : Prop

Used by: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.instInfiniteColimit, Structure.Arithmetic.Tower.instPeanoColimit, Structure.Arithmetic.Tower.levelFinite, Structure.Arithmetic.finTower, Structure.Arithmetic.instNonPeanoFin, Structure.Arithmetic.terminates_of_finite, Structure.Arithmetic.ultrafinitism, Tower, arithTower

A set is finite if the corresponding Subtype is finite, i.e., if there exists a natural n : ℕ and an equivalence s ≃ Fin n.

def Set.Finite.{u} {α : Type u} (s : Set α) : Prop

Used by: Structure.Arithmetic.Arith, Structure.Arithmetic.Terminates, Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.ultrafinitism

Constructor for Set.Finite using a Finite instance.

theorem Set.toFinite.{u} {α : Type u} (s : Set α) [Finite ↑s] : s.Finite

Used by: Structure.Arithmetic.instArithFin, Structure.Arithmetic.terminates_of_finite, Topology.step_conserves

theorem not_finite_iff_infinite.{u_1} {α : Sort u_1} : ¬Finite α ↔ Infinite α

Used by: Structure.Arithmetic.Tower.instInfiniteColimit, Structure.Arithmetic.Tower.instPeanoColimit

Data.Finset.Attach

attach s takes the elements of s and forms a new set of elements of the subtype {x // x ∈ s}.

def Finset.attach.{u_1} {α : Type u_1} (s : Finset α) : Finset ↥s

Used by: instNormValue

Data.Finset.BooleanAlgebra

theorem Finset.univ_eq_empty.{u_1} {α : Type u_1} [Fintype α] [IsEmpty α] : Finset.univ = ∅

Used by: Component.empty

theorem Finset.univ_nonempty.{u_1} {α : Type u_1} [Fintype α] [Nonempty α] : Finset.univ.Nonempty

Used by: Channel.maxWireSize

Data.Finset.Card

s.card is the number of elements of s, aka its cardinality.

The notation #s can be accessed in the Finset locale.

def Finset.card.{u_1} {α : Type u_1} (s : Finset α) : ℕ

Used by: ApplicationLayer.interface, BitSequence.trueCount, BitSequence.trueCount_le, Receiver.step, Sender.step

theorem Finset.card_filter_le.{u_1} {α : Type u_1} (s : Finset α) (p : α → Prop) [DecidablePred p] :
  (Finset.filter p s).card ≤ s.card

Used by: BitSequence.trueCount_le

theorem Finset.card_le_card.{u_1} {α : Type u_1} {s t : Finset α} : s ⊆ t → s.card ≤ t.card

Used by: ApplicationLayer.interface

theorem Finset.card_lt_card.{u_1} {α : Type u_1} {s t : Finset α} (h : s ⊂ t) : s.card < t.card

Used by: BitSequence.trueCount_strict

theorem Finset.card_singleton.{u_1} {α : Type u_1} (a : α) : {a}.card = 1

Used by: ApplicationLayer.interface

Data.Finset.Dedup

theorem Finset.mem_toList.{u_1} {α : Type u_1} {a : α} {s : Finset α} : a ∈ s.toList ↔ a ∈ s

Used by: Logic.PropositionalLogic.Formula.dnf_val

Produce a list of the elements in the finite set using choice.

def Finset.toList.{u_1} {α : Type u_1} (s : Finset α) : List α

Used by: Logic.PropositionalLogic.Formula.dnf, Logic.PropositionalLogic.Formula.dnf_val

Data.Finset.Defs

theorem Finset.ext.{u_1} {α : Type u_1} {s₁ s₂ : Finset α} (h : ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂) : s₁ = s₂

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.tensor

theorem Finset.ext_iff.{u_1} {α : Type u_1} {s₁ s₂ : Finset α} : s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂

Used by: BitSequence.trueCount_strict

Data.Finset.Disjoint

disjUnion s t h is the set such that a ∈ disjUnion s t h iff a ∈ s or a ∈ t. It is the same as s ∪ t, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

def Finset.disjUnion.{u_2} {α : Type u_2} (s t : Finset α) (h : Disjoint s t) : Finset α

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr

theorem Finset.disjoint_left.{u_2} {α : Type u_2} {s t : Finset α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Used by: InterfaceOld.Value.join_disjoint

theorem Finset.mem_disjUnion.{u_5} {α : Type u_5} {s t : Finset α} {h : Disjoint s t} {a : α} :
  a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t

Used by: InterfaceOld.Value.join

Data.Finset.Empty

A Finset for an empty type is empty.

theorem Finset.eq_empty_of_isEmpty.{u_1} {α : Type u_1} [IsEmpty α] (s : Finset α) : s = ∅

Used by: InterfaceOld.unit.Value.subsingleton

theorem Finset.notMem_empty.{u_1} {α : Type u_1} (a : α) : a ∉ ∅

Used by: instNonemptyValue

Data.Finset.Filter

Finset.filter p s is the set of elements of s that satisfy p.

For example, one can use s.filter (· ∈ t) to get the intersection of s with t : Set α as a Finset α (when a DecidablePred (· ∈ t) instance is available).

def Finset.filter.{u_1} {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset α

Used by: BitSequence.trueCount, BitSequence.trueCount_strict

theorem Finset.mem_filter.{u_1} {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} {a : α} :
  a ∈ Finset.filter p s ↔ a ∈ s ∧ p a

Used by: BitSequence.trueCount_strict

Data.Finset.Image

When f is an embedding of α in β and s is a finset in α, then s.map f is the image finset in β. The embedding condition guarantees that there are no duplicates in the image.

def Finset.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : Finset β

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr

theorem Finset.mem_map.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β} :
  b ∈ Finset.map f s ↔ ∃ a ∈ s, f a = b

Used by: InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint

Data.Finset.Insert

theorem Finset.mem_insert_of_mem.{u_1} {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (h : a ∈ s) :
  a ∈ insert b s

Used by: Logic.FirstOrderLogic.exists_fresh_ne

theorem Finset.mem_insert_self.{u_1} {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : a ∈ insert a s

Used by: Logic.FirstOrderLogic.exists_fresh_ne

Data.Finset.Lattice.Fold

theorem Finset.le_sup.{u_2, u_3} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α]
  {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) : f b ≤ s.sup f

Used by: Tower.structBot, Tower.structTop

Supremum of a finite set: sup {a, b, c} f = f a ⊔ f b ⊔ f c

def Finset.sup.{u_2, u_3} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β)
  (f : β → α) : α

Used by: Tower.structBot, Tower.structTop

Given nonempty finset s then s.sup' H f is the supremum of its image under f in (possibly unbounded) join-semilattice α, where H is a proof of nonemptiness. If α has a bottom element you may instead use Finset.sup which does not require s nonempty.

def Finset.sup'.{u_2, u_3} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (s : Finset β)
  (H : s.Nonempty) (f : β → α) : α

Used by: Channel.maxWireSize

Data.Finset.Preimage

theorem Finset.mem_preimage.{u, v} {α : Type u} {β : Type v} {f : α → β} {s : Finset β}
  {hf : Set.InjOn f (f ⁻¹' ↑s)} {x : α} : x ∈ s.preimage f hf ↔ f x ∈ s

Used by: InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor

Preimage of s : Finset β under a map f injective on f ⁻¹' s as a Finset.

def Finset.preimage.{u, v} {α : Type u} {β : Type v} (s : Finset β) (f : α → β)
  (hf : Set.InjOn f (f ⁻¹' ↑s)) : Finset α

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor

theorem Finset.preimage_empty.{u, v} {α : Type u} {β : Type v} {f : α → β} : ∅.preimage f ⋯ = ∅

Used by: InterfaceOld.tensor

theorem Finset.preimage_inl.{u, v} {α : Type u} {β : Type v} (s : Finset (α ⊕ β)) :
  s.preimage Sum.inl ⋯ = s.toLeft

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.tensor

theorem Finset.preimage_inr.{u, v} {α : Type u} {β : Type v} (s : Finset (α ⊕ β)) :
  s.preimage Sum.inr ⋯ = s.toRight

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inr, InterfaceOld.tensor

Data.Finset.Sum

Given a finset of elements α ⊕ β, extract all the elements of the form α. This forms a quasi-inverse to disjSum, in that it recovers its left input.

See also List.partitionMap.

def Finset.toLeft.{u_1, u_2} {α : Type u_1} {β : Type u_2} (u : Finset (α ⊕ β)) : Finset α

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.tensor

Given a finset of elements α ⊕ β, extract all the elements of the form β. This forms a quasi-inverse to disjSum, in that it recovers its right input.

See also List.partitionMap.

def Finset.toRight.{u_1, u_2} {α : Type u_1} {β : Type u_2} (u : Finset (α ⊕ β)) : Finset β

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inr, InterfaceOld.tensor

Data.Fintype.BigOperators

theorem Fintype.card_fun.{u_1, u_2} {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] :
  Fintype.card (α → β) = Fintype.card β ^ Fintype.card α

Used by: BitFunction.cardinality, BitSequence.cardinality, phoneNumber_cardinality

Data.Fintype.Card

theorem Finite.injective_iff_surjective.{u_1} {α : Type u_1} [Finite α] {f : α → α} :
  Function.Injective f ↔ Function.Surjective f

Used by: Cell.erase_not_surjective

theorem Fintype.card_bool : Fintype.card Bool = 2

Used by: BitSequence.cardinality

theorem Fintype.card_lt_of_injective_not_surjective.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Fintype α]
  [Fintype β] (f : α → β) (h : Function.Injective f) (h' : ¬Function.Surjective f) :
  Fintype.card α < Fintype.card β

Used by: Structure.Arithmetic.Tower.lt_card_level, Tower.card_lt_stepNeg, Tower.card_lt_stepPos

Data.Fintype.Defs

theorem Finset.mem_univ.{u_1} {α : Type u_1} [Fintype α] (x : α) : x ∈ Finset.univ

Used by: BitSequence.trueCount_strict, InterfaceOld.Value.observeAll, Logic.PropositionalLogic.Formula.dnf_val, Tower.structBot, Tower.structTop

Fintype α means that α is finite, i.e. there are only finitely many distinct elements of type α. The evidence of this is a finset elems (a list up to permutation without duplicates), together with a proof that everything of type α is in the list.

structure Fintype.{u_4} (α : Type u_4) : Type u_4

Used by: BitSequence.trueCount_strict, Channel.capacity, Channel.maxWireSize, FiniteStateMachine, FiniteStateMachine.Reversible, HeapCover.whole, HeapCover.whole_at, HeapCover.whole_domain, InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, Structure.Arithmetic.Tower.lt_card_level, Topology.Step.coverageFunctor, Topology.leave_preserves_connected, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck, Topology.step_conserves, instFintypeCell

Data.Fintype.EquivFin

Noncomputably get a Fintype instance from a Finite instance. This is not an instance because we want Fintype instances to be useful for computations.

def Fintype.ofFinite.{u_4} (α : Type u_4) [Finite α] : Fintype α

Used by: Structure.Arithmetic.Tower.lt_card_level, Tower.card_lt_stepNeg, Tower.card_lt_stepPos

theorem Infinite.of_injective.{u_4, u_5} {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : β → α)
  (hf : Function.Injective f) : Infinite α

Used by: SeqColimit.infinite

Data.Fintype.Lattice

theorem Finite.exists_max.{u_2, u_3} {α : Type u_2} {β : Type u_3} [Finite α] [Nonempty α] [LinearOrder β]
  (f : α → β) : ∃ x₀, ∀ (x : α), f x ≤ f x₀

Used by: Structure.Arithmetic.ultrafinitism

Data.Fintype.Pigeonhole

The pigeonhole principle for finitely many pigeons and pigeonholes. This is the Fintype version of Finset.exists_ne_map_eq_of_card_lt_of_maps_to.

theorem Fintype.exists_ne_map_eq_of_card_lt.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β]
  (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y

Used by: InformationSystem.exists_repeat_state

Data.Int.Cast.Basic

theorem Int.cast_natCast.{u} {R : Type u} [AddGroupWithOne R] (n : ℕ) : ↑↑n = ↑n

Used by: irrational_logb_two_five, irrational_logb_two_three

theorem Nat.cast_sub.{u} {R : Type u} [AddGroupWithOne R] {m n : ℕ} (h : m ≤ n) : ↑(n - m) = ↑n - ↑m

Used by: Topology.step_conserves

Data.Int.Cast.Defs

An AddGroupWithOne is an AddGroup with a 1. It also contains data for the unique homomorphisms ℕ → R and ℤ → R.

structure AddGroupWithOne.{u} (R : Type u) : Type u

Used by: Topology.step_conserves

Data.List.Basic

theorem List.map_injective_iff.{u, v} {α : Type u} {β : Type v} {f : α → β} :
  Function.Injective (List.map f) ↔ Function.Injective f

Used by: Frame.crc32Ethernet_detects_single_bit_flip

Data.List.Forall2

theorem List.forall₂_same.{u_1} {α : Type u_1} {Rₐ : α → α → Prop} {l : List α} :
  List.Forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x

Used by: Logic.Popper.Basis1.forall₂_mutual_refl

theorem List.rel_append.{u_1, u_2} {α : Type u_1} {β : Type u_2} {R : α → β → Prop} :
  Relator.LiftFun (List.Forall₂ R) (Relator.LiftFun (List.Forall₂ R) (List.Forall₂ R))
    (fun x1 x2 => x1 ++ x2) fun x1 x2 => x1 ++ x2

Used by: Logic.Popper.Basis1.demonstrate_congr_premise

Data.Nat.Basic

theorem Nat.leRecOn_injective.{u_1} {C : ℕ → Sort u_1} {n m : ℕ} (hnm : n ≤ m)
  (next : {k : ℕ} → C k → C (k + 1)) (Hnext : ∀ (n : ℕ), Function.Injective next) :
  Function.Injective (Nat.leRecOn hnm fun {k} => next)

Used by: SeqColimit.freshSeq_lt_ne, SeqColimit.mk_injective

Data.Nat.Cast.Defs

theorem Nat.cast_add.{u_1} {R : Type u_1} [AddMonoidWithOne R] (m n : ℕ) : ↑(m + n) = ↑m + ↑n

Used by: Discrete.prod, Topology.step_conserves

Data.Nat.Init

A type class for natural numbers which are greater than or equal to 2.

NeZero and AtLeastTwo are used for numeric literals, and also for groups of related lemmas sharing a common value of n that needs to be nonzero, or at least 2, and where it is convenient to pass this information implicitly. Instances for these classes cover some of the cases where it is most structurally obvious from the syntactic form of n that it satisfies the required conditions, such as m + 1. Less widely used cases may be defined as lemmas rather than global instances and then made into instances locally where needed. If implicit arguments, appearing before other explicit arguments, are allowed to be autoParams in a future version of Lean, such an autoParam that is proved by lia might be a more general replacement for the use of typeclass inference for this purpose.

structure Nat.AtLeastTwo (n : ℕ) : Prop

Used by: Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Z_iff_zero_fin, Structure.Arithmetic.instArithFin, Structure.Arithmetic.instNeZeroNat_structure, Structure.Arithmetic.instNonPeanoFin

Recursion starting at a non-zero number: given a map C k → C (k + 1) for each k, there is a map from C n to each C m, n ≤ m. For a version where the assumption is only made when k ≥ n, see Nat.leRec.

def Nat.leRecOn.{u_1} {C : ℕ → Sort u_1} {n m : ℕ} : n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m

Used by: SeqColimit.stepTo, Structure.Arithmetic.Tower.stepTo, arithStepTo_val

theorem Nat.leRecOn_self.{u_1} {C : ℕ → Sort u_1} {n : ℕ} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) :
  Nat.leRecOn ⋯ (fun {k} => next) x = x

Used by: SeqColimit.stepTo_self, Structure.Arithmetic.Tower.stepTo_self, arithStepTo_val

theorem Nat.leRecOn_succ.{u_1} {C : ℕ → Sort u_1} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1}
  {next : {k : ℕ} → C k → C (k + 1)} (x : C n) :
  Nat.leRecOn h2 next x = next (Nat.leRecOn h1 (fun {k} => next) x)

Used by: SeqColimit.stepTo_succ, Structure.Arithmetic.Tower.stepTo_succ

theorem Nat.leRecOn_trans.{u_1} {C : ℕ → Sort u_1} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k)
  {next : {k : ℕ} → C k → C (k + 1)} (x : C n) :
  Nat.leRecOn ⋯ next x = Nat.leRecOn hmk next (Nat.leRecOn hnm next x)

Used by: SeqColimit.stepTo_trans, Structure.Arithmetic.Tower.stepTo_trans

Induction principle starting at a non-zero number. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

This is an alias of Nat.leRec, specialized to Prop.

theorem Nat.le_induction {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop} (base : P m ⋯)
  (succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) (n : ℕ) (hmn : m ≤ n) : P n hmn

Used by: BitFunction.iterate_stays, Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff

Data.Nat.Prime.Defs

Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. The theorem Nat.prime_def witnesses this description of a prime number.

def Nat.Prime (p : ℕ) : Prop

Used by: instFactPrimeOfNatNat_computerNetworks

theorem Nat.prime_two : Nat.Prime 2

Used by: instFactPrimeOfNatNat_computerNetworks

Data.Prod.Basic

theorem Prod.mk.eta.{u_1, u_2} {α : Type u_1} {β : Type u_2} {p : α × β} : (p.1, p.2) = p

Used by: Component.recast

Data.Quot

Map a function f : α → β that sends equivalent elements to equivalent elements to a function Quotient sa → Quotient sb. Useful to define unary operations on quotients.

def Quotient.map.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : α → β)
  (h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b) : Quotient sa → Quotient sb

Used by: Component.Hom.recast

Map a function f : α → β → γ that sends equivalent elements to equivalent elements to a function f : Quotient sa → Quotient sb → Quotient sc. Useful to define binary operations on quotients.

def Quotient.map₂.{u_1, u_2, u_4} {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β}
  {γ : Sort u_4} {sc : Setoid γ} (f : α → β → γ)
  (h : ∀ ⦃a₁ a₂ : α⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂ : β⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
  Quotient sa → Quotient sb → Quotient sc

Used by: Component.Hom.comp, Component.Hom.tensor

Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

def Quotient.out.{u_1} {α : Sort u_1} {s : Setoid α} : Quotient s → α

Used by: Tower.structBot, Tower.structTop

Data.Rat.Cast.Defs

theorem Rat.cast_intCast.{u_3} {α : Type u_3} [DivisionRing α] (n : ℤ) : ↑↑n = ↑n

Used by: irrational_logb_two_five, irrational_logb_two_three

theorem Rat.cast_natCast.{u_3} {α : Type u_3} [DivisionRing α] (n : ℕ) : ↑↑n = ↑n

Used by: irrational_logb_two_five, irrational_logb_two_three

Data.Rat.Defs

theorem Rat.pos (a : ℚ) : 0 < a.den

Used by: irrational_logb_two_five, irrational_logb_two_three

Data.Real.Basic

The type ℝ of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.

structure Real : Type

Used by: Bit.discrete, Bool.discrete, Cell.eraseSecondBit, Channel.capacity, Channel.loss, Channel.lossless, Channel.lossless_stationary, Channel.lossy_loses_overall, Channel.maxWireSize, Channel.overall_loss, Component.Simplex.toInformationSystem, Component.empty, Component.id, Component.parallel, Component.parallel_comm, Component.recast, Component.sequential, Component.symmetry, Discrete, Discrete.pi, Discrete.prod, Discrete.size, Discrete.size_eq, InformationSystem, InformationSystem.Environment.universe, InformationSystem.Environment.universe_isolated, InformationSystem.Spontaneous, InformationSystem.Step.bottom, InformationSystem.Step.delta, InformationSystem.Step.delta_alt, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.delta, InformationSystem.eval_delta, InformationSystem.eval_trichotomy, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InformationSystem.isolated, InformationSystem.natural, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.parallel_delta, InformationSystem.perpetuous, InformationSystem.perpetuous_coherent, InformationSystem.roundtrip_neutral, InformationSystem.sequential_delta, InformationSystem.spontaneous_no_self_return, InformationSystem.spontaneous_not_perpetuous, InformationSystem.toSimplex, InformationSystem.zero_run_le, List.totalSize, NormNonneg, Receiver.step, Sender.step, Topology.step_conserves, Unit.discrete, instNormBit, instNormBool_computerNetworks, instNormCell, instNormEvent, instNormForallFin_computerNetworks, instNormFrame, instNormIcmp, instNormNonnegBit, instNormNonnegBool, instNormNonnegCell, instNormNonnegForallFin, instNormNonnegProd, instNormNonnegUnit, instNormPacket, instNormProd_computerNetworks, instNormProtocol, instNormSegment, instNormSetBlock, instNormSignal, instNormUnit_computerNetworks, instNormValue, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, irrational_trafficLightInformation, phoneNumberInformation, phoneNumberInformation_eq, trafficLightInformation, trafficLightInformation_eq

Data.Set.Basic

theorem Set.eq_univ_of_forall.{u} {α : Type u} {s : Set α} : (∀ (x : α), x ∈ s) → s = Set.univ

Used by: Structure.Arithmetic.ultrafinitism

theorem Set.inter_subset_left.{u} {α : Type u} {s t : Set α} : s ∩ t ⊆ s

Used by: Topology.nerveCoverage

theorem Set.inter_subset_right.{u} {α : Type u} {s t : Set α} : s ∩ t ⊆ t

Used by: Topology.isNerveCover_inter

theorem Set.mem_union.{u} {α : Type u} (x : α) (a b : Set α) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b

Used by: Heap.combine, Topology.join_preserves_connected

theorem Set.mem_union_left.{u} {α : Type u} {x : α} {a : Set α} (b : Set α) : x ∈ a → x ∈ a ∪ b

Used by: Heap.combine_at_left

theorem Set.mem_union_right.{u} {α : Type u} {x : α} {b : Set α} (a : Set α) : x ∈ b → x ∈ a ∪ b

Used by: Heap.combine_at_right

theorem Set.notMem_empty.{u} {α : Type u} (x : α) : x ∉ ∅

Used by: Heap.empty, arithTower

Data.Set.Card

The cardinality of s : Set α . Has the junk value 0 if s is infinite

def Set.ncard.{u_1} {α : Type u_1} (s : Set α) : ℕ

Used by: Topology.step_conserves, instNormSetBlock

theorem Set.ncard_insert_of_notMem.{u_1} {α : Type u_1} {s : Set α} {a : α} (h : a ∉ s)
  (hs : s.Finite := by toFinite_tac) : (insert a s).ncard = s.ncard + 1

Used by: Topology.step_conserves

theorem Set.ncard_pos.{u_1} {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) :
  0 < s.ncard ↔ s.Nonempty

Used by: Topology.step_conserves

theorem Set.ncard_sdiff_singleton_of_mem.{u_1} {α : Type u_1} {s : Set α} {a : α} (h : a ∈ s) :
  (s \ {a}).ncard = s.ncard - 1

Used by: Topology.step_conserves

Data.Set.CoeSort

Data.Set.Defs

A set is a collection of elements of some type α.

Although Set is defined as α → Prop, this is an implementation detail which should not be relied on. Instead, setOf and membership of a set (∈) should be used to convert between sets and predicates.

def Set.{u} (α : Type u) : Type u

Used by: Class, Class.Passive, Class.reachable, Heap, Heap.combine, Heap.combine_at_left, Heap.combine_at_right, Heap.combine_domain, Heap.create, Heap.create_delete, Heap.create_domain, Heap.delete, Heap.delete_domain, Heap.dematerialize, Heap.empty, Heap.materialize, Heap.materialize_dematerialize, Heap.mem_reachable, Heap.reachable, HeapCover.agree, HeapCover.whole, HeapCover.whole_at, HeapCover.whole_domain, Interface, Interface.combine, Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset, Object, Object.state, SimpleGraph.induceComplSingletonEquiv, Structure.Arithmetic.Orbit, Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.exists_S_of_not_Z, Structure.Arithmetic.instArithFin, Structure.Arithmetic.instDefS, Structure.Arithmetic.lt_wf, Structure.Arithmetic.orbit_le, Structure.Arithmetic.orbit_subset, Structure.Arithmetic.terminates_iff_bounded, Structure.Arithmetic.terminates_of_finite, Structure.Arithmetic.terminates_of_halts, Structure.Arithmetic.terminates_of_le, Structure.Arithmetic.ultrafinitism, Topology.Coverage, Topology.IsNerveCover, Topology.Step.coverageFunctor, Topology.isNerveCover_inter, Topology.joinCoverage, Topology.joinFunctor, Topology.joinGrothendieck, Topology.joinHistory, Topology.join_preserves_connected, Topology.leaveCoverage, Topology.leave_preserves_connected, Topology.membership, Topology.nerveCoverage, Topology.nerveTopology, Topology.restrict, Topology.restrictPresieve, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck, Topology.step, Topology.step_conserves, Tower, Tower.heapBot, Tower.heapTop, Tower.wholeHeap, arithTower, doorBehavior, doorHeap, doorHeap.closedVal, doorHeap.closed_reachable, doorHeap.openedVal, doorHeap.opened_reachable, doorInterface, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass, instNormSetBlock, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap, irrational_logb_two_five, irrational_logb_two_three

The property s.Nonempty expresses the fact that the set s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

def Set.Nonempty.{u} {α : Type u} (s : Set α) : Prop

Used by: Structure.Arithmetic.lt_wf, Topology.step_conserves

theorem Set.ext.{u} {α : Type u} {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b

Used by: Heap.create_delete, Topology.join_preserves_connected

The image of s : Set α by f : α → β, written f '' s, is the set of b : β such that f a = b for some a ∈ s.

def Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set β

Used by: Topology.joinCoverage

The universal set on a type α is the set containing all elements of α.

This is conceptually the “same as” α (in set theory, it is actually the same), but type theory makes the distinction that α is a type while Set.univ is a term of type Set α. Set.univ can itself be coerced to a type ↥Set.univ which is in bijection with (but distinct from) α.

def Set.univ.{u} {α : Type u} : Set α

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne, Structure.Arithmetic.ultrafinitism, doorClass, doorHeap

Data.Set.Finite.Basic

theorem Set.Finite.insert.{u} {α : Type u} (a : α) {s : Set α} (hs : s.Finite) : (insert a s).Finite

Used by: Structure.Arithmetic.terminates_of_halts

theorem Set.Infinite.exists_notMem_finset.{u} {α : Type u} {s : Set α} (hs : s.Infinite) (t : Finset α) :
  ∃ a ∈ s, a ∉ t

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne

theorem Set.finite_singleton.{u} {α : Type u} (a : α) : {a}.Finite

Used by: Structure.Arithmetic.terminates_of_halts

theorem Set.finite_univ_iff.{u} {α : Type u} : Set.univ.Finite ↔ Finite α

Used by: Structure.Arithmetic.ultrafinitism

theorem Set.infinite_univ.{u} {α : Type u} [h : Infinite α] : Set.univ.Infinite

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne

Data.Set.Finite.Lemmas

theorem Set.exists_max_image.{u, v} {α : Type u} {β : Type v} [LinearOrder β] (s : Set α) (f : α → β)
  (h1 : s.Finite) : s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

Used by: Structure.Arithmetic.exists_S_of_not_Z, Structure.Arithmetic.terminates_iff_bounded

theorem Set.exists_min_image.{u, v} {α : Type u} {β : Type v} [LinearOrder β] (s : Set α) (f : α → β)
  (h1 : s.Finite) : s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b

Used by: Structure.Arithmetic.instDefS, Structure.Arithmetic.lt_wf

Data.Set.Finite.Range

theorem Set.finite_range.{u, w} {α : Type u} {ι : Sort w} (f : ι → α) [Finite ι] : (Set.range f).Finite

Used by: Structure.Arithmetic.Tower.instArithColimit

Data.Set.Function

Alias of Set.injOn_of_injective.

theorem Function.Injective.injOn.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β}
  (h : Function.Injective f) {s : Set α} : Set.InjOn f s

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor

Data.Set.Image

theorem Set.image_mono.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α} (h : s ⊆ t) :
  f '' s ⊆ f '' t

Used by: Topology.joinCoverage

Data.Set.Inclusion

inclusion is the “identity” function between two subsets s and t, where s ⊆ t

abbrev Set.inclusion.{u_1} {α : Type u_1} {s t : Set α} (h : s ⊆ t) : ↑s → ↑t

Used by: Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset

Data.Set.Insert

theorem Set.mem_insert.{u_1} {α : Type u_1} (x : α) (s : Set α) : x ∈ insert x s

Used by: Heap.create_delete, Heap.materialize_dematerialize, Structure.Arithmetic.orbit_subset

theorem Set.mem_insert_iff.{u_1} {α : Type u_1} {x a : α} {s : Set α} : x ∈ insert a s ↔ x = a ∨ x ∈ s

Used by: Heap.create, Heap.create_delete, Topology.join_preserves_connected

theorem Set.mem_insert_of_mem.{u_1} {α : Type u_1} {x : α} {s : Set α} (y : α) : x ∈ s → x ∈ insert y s

Used by: Structure.Arithmetic.orbit_subset, Topology.joinCoverage

theorem Set.mem_singleton_iff.{u_1} {α : Type u_1} {a b : α} : a ∈ {b} ↔ a = b

Used by: Heap.create_delete, Topology.join_preserves_connected

Data.Set.Lattice

theorem Set.iUnion_subset_iff.{u_1, u_5} {α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {t : Set α} :
  ⋃ i, s i ⊆ t ↔ ∀ (i : ι), s i ⊆ t

Used by: Topology.isNerveCover_inter

Data.Set.Operations

f is injective on s if the restriction of f to s is injective.

def Set.InjOn.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Prop

Used by: InterfaceOld.tensor

theorem Set.mem_sdiff.{u} {α : Type u} {s t : Set α} (x : α) : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t

Used by: Heap.create_delete

The preimage of s : Set β by f : α → β, written f ⁻¹' s, is the set of x : α such that f x ∈ s.

def Set.preimage.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set β) : Set α

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor

Range of a function.

This function is more flexible than f '' univ, as the image requires that the domain is in Type and not an arbitrary Sort.

def Set.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set α

Used by: Structure.Arithmetic.Tower.instArithColimit, irrational_logb_two_five, irrational_logb_two_three

Data.Subtype

theorem Subtype.heq_iff_coe_eq.{u_1} {α : Sort u_1} {p q : α → Prop} (h : ∀ (x : α), p x ↔ q x)
  {a1 : { x // p x }} {a2 : { x // q x }} : a1 ≍ a2 ↔ ↑a1 = ↑a2

Used by: InterfaceOld.Value.ext_of_fired_eq

Data.Sum.Basic

Data.ZMod.Defs

Logic.Basic

Any prop p is decidable classically. A shorthand for Classical.propDecidable.

def Classical.dec (p : Prop) : Decidable p

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instPeanoStandard

Wrapper for adding elementary propositions to the type class systems. Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally, but sometimes it is very convenient to be able to use the type class system in specific circumstances.

For example, ZMod p is a field if and only if p is a prime number. In order to be able to find this field instance automatically by type class search, we have to turn p.Prime into an instance implicit assumption.

On the other hand, making Nat.Prime a class would require a major refactoring of the library, and it is questionable whether making Nat.Prime a class is desirable at all. The compromise is to add the assumption [Fact p.Prime] to ZMod.instField.

In particular, this class is not intended for turning the type class system into an automated theorem prover for first-order logic.

structure Fact (p : Prop) : Prop

Used by: instFactPrimeOfNatNat_computerNetworks

theorem eq_or_ne.{u_1} {α : Sort u_1} (x y : α) : x = y ∨ x ≠ y

Used by: Frame.ofFn_update, Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.realize_SUB

Logic.Embedding.Basic

α ↪ β is a bundled injective function.

structure Function.Embedding.{u_1, u_2} (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr

Logic.Equiv.Basic

theorem Function.update_comp_equiv.{u_1, u_4, u_9} {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9}
  [DecidableEq α'] [DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) :
  Function.update f a v ∘ ⇑g = Function.update (f ∘ ⇑g) (g.symm a) v

Used by: Frame.crc32Ethernet_detects_single_bit_flip

Logic.Equiv.Defs

α ≃ β is the type of functions from α → β with a two-sided inverse.

structure Equiv.{u_1, u_2} (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.reflectEquiv_symm, SimpleGraph.induceComplSingletonEquiv, arithLevelTopEquivNat

Perm α is the type of bijections from α to itself.

abbrev Equiv.Perm.{u_1} (α : Sort u_1) : Sort (max 1 u_1)

Used by: Frame.crc32Ethernet, Frame.crc32Ethernet_detects_single_bit_flip, Frame.reflectEquiv

theorem Equiv.injective.{u, v} {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Injective ⇑e

Used by: arithToNat_injective

Inverse of an equivalence e : α ≃ β.

def Equiv.symm.{u, v} {α : Sort u} {β : Sort v} (e : α ≃ β) : β ≃ α

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.reflectEquiv_symm

Logic.Function.Basic

theorem Function.hfunext.{u, v} {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : (a : α) → β a}
  {f' : (a : α') → β' a} (hα : α = α') (h : ∀ (a : α) (a' : α'), a ≍ a' → f a ≍ f' a') : f ≍ f'

Used by: InterfaceOld.Value.ext_of_fired_eq, InterfaceOld.unit.Value.subsingleton

The inverse of a function (which is a left inverse if f is injective and a right inverse if f is surjective).

def Function.invFun.{u, u_3} {α : Sort u} {β : Sort u_3} [Nonempty α] (f : α → β) : β → α

Used by: InformationSystem.reversible

theorem Function.leftInverse_invFun.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β}
  (hf : Function.Injective f) : Function.LeftInverse (Function.invFun f) f

Used by: InformationSystem.reversible

theorem Function.update_comm.{u_1, u_2} {α : Sort u_2} [DecidableEq α] {β : α → Sort u_1} {a b : α}
  (h : a ≠ b) (v : β a) (w : β b) (f : (a : α) → β a) :
  Function.update (Function.update f a v) b w = Function.update (Function.update f b w) a v

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal

A congruence lemma for Function.update, specialized for the non-dependent case. Without this, simp can’t rewrite in the fourth argument a because the result type depends on a. See also https://github.com/leanprover/lean4/issues/12478.

theorem Function.update_congr.{u, u_1} {α : Sort u} [DecidableEq α] {β : Sort u_1} {f₁ f₂ : α → β}
  (hf : f₁ = f₂) {a'₁ a'₂ : α} (ha' : a'₁ = a'₂) {v₁ v₂ : β} (hv : v₁ = v₂) {a₁ a₂ : α}
  (ha : a₁ = a₂) : Function.update f₁ a'₁ v₁ a₁ = Function.update f₂ a'₂ v₂ a₂

Used by: Logic.PropositionalLogic.Formula.eliminate

theorem Function.update_eq_self.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (a : α)
  (f : (a : α) → β a) : Function.update f a (f a) = f

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.realize_nonDep_update

theorem Function.update_idem.{u_1, u_2} {α : Sort u_2} [DecidableEq α] {β : α → Sort u_1} {a : α}
  (v w : β a) (f : (a : α) → β a) :
  Function.update (Function.update f a v) a w = Function.update f a w

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.realize_nonDep_update, Logic.FirstOrderLogic.realize_update_of_nonDep

theorem Function.update_of_ne.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] {a a' : α} (h : a ≠ a')
  (v : β a') (f : (a : α) → β a) : Function.update f a' v a = f a

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_update_of_nonDep, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset, Logic.PropositionalLogic.Formula.eliminate

theorem Function.update_self.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (a : α) (v : β a)
  (f : (a : α) → β a) : Function.update f a v a = v

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal, Logic.FirstOrderLogic.realize_SUB, Logic.PropositionalLogic.Formula.eliminate

Logic.Function.Iterate

theorem Function.iterate_succ_apply'.{u} {α : Type u} (f : α → α) (n : ℕ) (x : α) :
  f^[n.succ] x = f (f^[n] x)

Used by: BitFunction.fixedPoint_isFixed, BitFunction.iterate_dominates_succ, BitFunction.iterate_stays, Structure.Arithmetic.count_succ

Iterate a function.

def Nat.iterate.{u} {α : Sort u} (op : α → α) : ℕ → α → α

Used by: BitFunction.fixedPoint_isFixed, BitFunction.iterate, BitFunction.iterate_dominates_succ, BitFunction.iterate_stays, Structure.Arithmetic.count

Logic.IsEmpty.Defs

IsEmpty α expresses that α is empty.

structure IsEmpty.{u} (α : Sort u) : Prop

Used by: instIsEmptyPortsUnit_computerChips

Logic.Nonempty

Using Classical.choice, extracts a term from a Nonempty type.

abbrev Classical.arbitrary.{u_3} (α : Sort u_3) [h : Nonempty α] : α

Used by: Layer.trace_vanishing, Layer.trace_yanking

Using Classical.choice, extracts a term from a Nonempty type.

abbrev Nonempty.some.{u_3} {α : Sort u_3} (h : Nonempty α) : α

Used by: Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.derivable_iff_derivableCutFree, Logic.ProofTheory.toBasis1, Logic.PropositionalLogic.derivable_mp, Structure.Arithmetic.instNonPeanoFin

Logic.Nontrivial.Defs

Predicate typeclass for expressing that a type is not reduced to a single element. In rings, this is equivalent to 0 ≠ 1. In vector spaces, this is equivalent to positive dimension.

structure Nontrivial.{u_3} (α : Type u_3) : Prop

Used by: Structure.Arithmetic.Arith, Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.lt_card_level

theorem exists_ne.{u_1} {α : Type u_1} [Nontrivial α] (x : α) : ∃ y, y ≠ x

Used by: Logic.FirstOrderLogic.realize_nonDep_update

Logic.Relation

ReflTransGen r: reflexive transitive closure of r

inductive Relation.ReflTransGen.{u_1} {α : Type u_1} (r : α → α → Prop) (a : α) : α → Prop

Used by: Structure.Arithmetic.Orbit, Structure.Arithmetic.orbit_le, Structure.Arithmetic.orbit_subset, Structure.Arithmetic.terminates_of_halts

theorem Relation.ReflTransGen.cases_head.{u_1} {α : Type u_1} {r : α → α → Prop} {a b : α}
  (h : Relation.ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ Relation.ReflTransGen r c b

Used by: Structure.Arithmetic.orbit_subset, Structure.Arithmetic.terminates_of_halts

ModelTheory.Basic

ModelTheory.LanguageMap

A language homomorphism maps the symbols of one language to symbols of another.

structure FirstOrder.Language.LHom.{u, v, u', v'} (L : FirstOrder.Language) (L' : FirstOrder.Language) :
  Type (max (max (max u u') v) v')

Used by: Tower, Tower.lang0ToBot, Tower.lang0ToTop

The identity language homomorphism.

def FirstOrder.Language.LHom.id.{u_1, u_2} (L : FirstOrder.Language) : L →ᴸ L

Used by: arithTower

ModelTheory.Semantics

A bounded formula can be evaluated as true or false by giving values to each free and bound variable.

def FirstOrder.Language.BoundedFormula.Realize.{u, v, w, u'} {L : FirstOrder.Language} {M : Type w}
  [L.Structure M] {α : Type u'} {l : ℕ} (_f : L.BoundedFormula α l) (_v : α → M) (_xs : Fin l → M) :
  Prop

Used by: Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset

A special case of realize_restrictFreeVar, included because we can add the simp attribute to it

theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar'.{u, v, w, u'} {L : FirstOrder.Language}
  {M : Type w} [L.Structure M] {α : Type u'} [DecidableEq α] {n : ℕ} {φ : L.BoundedFormula α n}
  {s : Set α} (h : ↑φ.freeVarFinset ⊆ s) {v : α → M} {xs : Fin n → M} :
  (φ.restrictFreeVar (Set.inclusion h)).Realize (v ∘ Subtype.val) xs ↔ φ.Realize v xs

Used by: Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset

theorem FirstOrder.Language.BoundedFormula.realize_subst.{u, v, w, u', v'} {L : FirstOrder.Language}
  {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ} {φ : L.BoundedFormula α n}
  {tf : α → L.Term β} {v : β → M} {xs : Fin n → M} :
  (φ.subst tf).Realize v xs ↔ φ.Realize (fun a => FirstOrder.Language.Term.realize v (tf a)) xs

Used by: Logic.FirstOrderLogic.realize_SUB

theorem FirstOrder.Language.Formula.realize_iAlls.{u, v, w, u', v'} {L : FirstOrder.Language} {M : Type w}
  [L.Structure M] {α : Type u'} {β : Type v'} [Finite β] {φ : L.Formula (α ⊕ β)} {v : α → M} :
  (FirstOrder.Language.Formula.iAlls β φ).Realize v ↔
    ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Used by: Logic.FirstOrderLogic.realize_all

theorem FirstOrder.Language.Formula.realize_iExs.{u, v, w, u', u_3} {L : FirstOrder.Language} {M : Type w}
  [L.Structure M] {α : Type u'} {γ : Type u_3} [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} :
  (FirstOrder.Language.Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)

Used by: Logic.FirstOrderLogic.realize_ex

theorem FirstOrder.Language.Formula.realize_relabel.{u, v, w, u', v'} {L : FirstOrder.Language} {M : Type w}
  [L.Structure M] {α : Type u'} {β : Type v'} {φ : L.Formula α} {g : α → β} {v : β → M} :
  (FirstOrder.Language.Formula.relabel g φ).Realize v ↔ φ.Realize (v ∘ g)

Used by: Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex

A term t with variables indexed by α can be evaluated by giving a value to each variable.

def FirstOrder.Language.Term.realize.{u, v, w, u'} {L : FirstOrder.Language} {M : Type w}
  [L.Structure M] {α : Type u'} (v : α → M) (_t : L.Term α) : M

Used by: Logic.FirstOrderLogic.realize_SUB

ModelTheory.Syntax

The Finset of free variables used in a given formula.

def FirstOrder.Language.BoundedFormula.freeVarFinset.{u, v, u'} {L : FirstOrder.Language} {α : Type u'}
  [DecidableEq α] {n : ℕ} : L.BoundedFormula α n → Finset α

Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset

Restricts a bounded formula to only use a particular set of free variables.

def FirstOrder.Language.BoundedFormula.restrictFreeVar.{u, v, u', v'} {L : FirstOrder.Language}
  {α : Type u'} {β : Type v'} [DecidableEq α] {n : ℕ} (φ : L.BoundedFormula α n)
  (_f : ↥φ.freeVarFinset → β) : L.BoundedFormula β n

Used by: Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset

Substitutes the free variables in a bounded formula with terms, leaving bound variables unchanged.

def FirstOrder.Language.BoundedFormula.subst.{u, v, u', v'} {L : FirstOrder.Language} {α : Type u'}
  {β : Type v'} {n : ℕ} (φ : L.BoundedFormula α n) (f : α → L.Term β) : L.BoundedFormula β n

Used by: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.realize_SUB

iAlls f φ transforms a L.Formula (α ⊕ β) into a L.Formula α by universally quantifying over all variables Sum.inr _.

def FirstOrder.Language.Formula.iAlls.{u, v, u', v'} {L : FirstOrder.Language} {α : Type u'}
  (β : Type v') [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formula α

Used by: Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.realize_all

iExs f φ transforms a L.Formula (α ⊕ β) into a L.Formula α by existentially quantifying over all variables Sum.inr _.

def FirstOrder.Language.Formula.iExs.{u, v, u', v'} {L : FirstOrder.Language} {α : Type u'}
  (β : Type v') [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formula α

Used by: Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.realize_ex

Relabels a formula’s variables along a particular function.

def FirstOrder.Language.Formula.relabel.{u, v, u', v'} {L : FirstOrder.Language} {α : Type u'}
  {β : Type v'} (g : α → β) : L.Formula α → L.Formula β

Used by: Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex

A term on α is either a variable indexed by an element of α or a function symbol applied to simpler terms.

inductive FirstOrder.Language.Term.{u, v, u'} (L : FirstOrder.Language) (α : Type u') : Type (max u u')

Used by: Logic.FirstOrderLogic.SUB, Logic.FirstOrderLogic.realize_SUB

NumberTheory.Real.Irrational

A real number is irrational if it is not equal to any rational number.

def Irrational (x : ℝ) : Prop

Used by: irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, irrational_trafficLightInformation

theorem Irrational.add_natCast {x : ℝ} (h : Irrational x) (m : ℕ) : Irrational (x + ↑m)

Used by: irrational_phoneNumberInformation

theorem Irrational.mul_natCast {x : ℝ} (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (x * ↑m)

Used by: irrational_phoneNumberInformation

Order.Basic

Alias of ge_of_eq.

theorem Eq.ge.{u_1} {α : Type u_1} [Preorder α] {a b : α} (hab : a = b) : b ≤ a

Used by: Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.ι_injective

Alias of le_of_eq.

theorem Eq.le.{u_1} {α : Type u_1} [Preorder α] {a b : α} (hab : a = b) : a ≤ b

Used by: Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.ι_injective

Order.BoundedOrder.Basic

An order is an OrderBot if it has a least element. We state this using a data mixin, holding the value of ⊥ and the least element constraint.

structure OrderBot.{u} (α : Type u) [LE α] : Type u

Used by: Structure.Arithmetic.Arith, Structure.Arithmetic.Tower.instOrderBotColimit

theorem bot_le.{u} {α : Type u} [LE α] [OrderBot α] {a : α} : ⊥ ≤ a

Used by: Structure.Arithmetic.Tower.instOrderBotColimit, Structure.Arithmetic.instDefS, Structure.Arithmetic.instDefZ, Structure.Arithmetic.ultrafinitism

Order.Defs.LinearOrder

A linear order is reflexive, transitive, antisymmetric and total relation ≤. We assume that every linear ordered type has decidable (≤), (<), and (=).

structure LinearOrder.{u_2} (α : Type u_2) : Type u_2

Used by: Structure.Arithmetic.Arith, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instDefS

theorem le_of_not_gt.{u_1} {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b < a) : a ≤ b

Used by: InformationSystem.Step.bottom, InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

theorem le_total.{u_1} {α : Type u_1} [LinearOrder α] (a b : α) : a ≤ b ∨ b ≤ a

Used by: Structure.Arithmetic.Tower.sigmaLe_total, Structure.Arithmetic.instDefS, Structure.Arithmetic.lt_wf

theorem lt_of_not_ge.{u_1} {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) : a < b

Used by: Channel.lossy_loses_overall, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.spontaneous_no_self_return

theorem lt_or_gt_of_ne.{u_1} {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≠ b) : a < b ∨ b < a

Used by: InformationSystem.exists_repeat_state

theorem lt_trichotomy.{u_1} {α : Type u_1} [LinearOrder α] (a b : α) : a < b ∨ a = b ∨ b < a

Used by: InformationSystem.Step.delta_trichotomy, InformationSystem.eval_trichotomy, SeqColimit.freshSeq_injective, Structure.Arithmetic.S_unique

theorem not_lt.{u_1} {α : Type u_1} [LinearOrder α] {a b : α} : ¬a < b ↔ b ≤ a

Used by: Structure.Arithmetic.lt_wf

Order.Defs.PartialOrder

Equality is decidable if ≤ is.

def decidableEqOfDecidableLE.{u_1} {α : Type u_1} [PartialOrder α] [DecidableLE α] : DecidableEq α

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instPeanoStandard

< is decidable if ≤ is.

def decidableLTOfDecidableLE.{u_1} {α : Type u_1} [Preorder α] [DecidableLE α] : DecidableLT α

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instPeanoStandard

theorem le_of_eq.{u_1} {α : Type u_1} [Preorder α] {a b : α} (hab : a = b) : a ≤ b

Used by: Structure.Arithmetic.Tower.step_le_iff

theorem le_of_lt.{u_1} {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) : a ≤ b

Used by: Structure.Arithmetic.exists_S_of_not_Z

The relation ≤ on a preorder is transitive.

theorem le_trans.{u_1} {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c

Used by: ApplicationLayer.interface

theorem lt_of_le_of_lt.{u_1} {α : Type u_1} [Preorder α] {a b c : α} (hab : a ≤ b) (hbc : b < c) : a < c

Used by: Frame.toPoly_degree_lt

theorem lt_trans.{u_1} {α : Type u_1} [Preorder α] {a b c : α} : a < b → b < c → a < c

Used by: Frame.toPoly_degree_lt

theorem ne_of_gt.{u_1} {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : a ≠ b

Used by: phoneNumberInformation_eq

Order.Disjoint

Two elements of a lattice are disjoint if their inf is the bottom element. (This generalizes disjoint sets, viewed as members of the subset lattice.)

Note that we define this without reference to ⊓, as this allows us to talk about orders where the infimum is not unique, or where implementing Inf would require additional Decidable arguments.

def Disjoint.{u_1} {α : Type u_1} [PartialOrder α] [OrderBot α] (a b : α) : Prop

Used by: Finset.sum_preimage_map_disjUnion, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint

Order.GaloisConnection.Defs

A Galois connection is a pair of functions l and u satisfying l a ≤ b ↔︎ a ≤ u b. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib.

def GaloisConnection.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] (l : α → β)
  (u : β → α) : Prop

Used by: Specification.galoisConnection

theorem GaloisConnection.monotone_l.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β}
  {l : β → α} (gc : GaloisConnection l u) : Monotone l

Used by: Specification.closed

theorem GaloisConnection.monotone_u.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β}
  {u : β → α} (gc : GaloisConnection l u) : Monotone u

Used by: Specification.closed

Order.Heyting.Basic

p → q → r ↔︎ q ∧ p → r

theorem le_himp_iff'.{u_2} {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} : a ≤ b ⇨ c ↔ b ⊓ a ≤ c

Used by: Specification.galoisConnection

Order.Hom.Basic

An order isomorphism is an equivalence such that a ≤ b ↔︎ (f a) ≤ (f b). This definition is an abbreviation of RelIso (≤) (≤).

abbrev OrderIso.{u_6, u_7} (α : Type u_6) (β : Type u_7) [LE α] [LE β] : Type (max u_6 u_7)

Used by: Structure.Arithmetic.peanoOrderIso

Order.Hom.Set

A strictly monotone surjective function from a linear order is an order isomorphism.

def StrictMono.orderIsoOfSurjective.{u_1, u_2} {α : Type u_1} {β : Type u_2} [LinearOrder α]
  [Preorder β] (f : α → β) (h_mono : StrictMono f) (h_surj : Function.Surjective f) : α ≃o β

Used by: Structure.Arithmetic.peanoOrderIso

Order.Interval.Finset.Defs

theorem Set.finite_Iic.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) :
  (Set.Iic a).Finite

Used by: Structure.Arithmetic.instArithNat

Order.Interval.Set.Defs

Order.Lattice

theorem inf_le_left.{u} {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b ≤ a

Used by: Specification.binaryCone

theorem inf_le_right.{u} {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b ≤ b

Used by: Specification.binaryCone

Order.MinMax

theorem max_lt_iff.{u} {α : Type u} [LinearOrder α] {a b c : α} : max b c < a ↔ b < a ∧ c < a

Used by: Frame.toPoly_degree_lt

Order.Monotone.Basic

theorem strictMono_nat_of_lt_succ.{u} {α : Type u} [Preorder α] {f : ℕ → α}
  (hf : ∀ (n : ℕ), f n < f (n + 1)) : StrictMono f

Used by: Structure.Arithmetic.count_strictMono

Order.Monotone.Defs

A function f is strictly monotone if a < b implies f a < f b.

def StrictMono.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) : Prop

Used by: Structure.Arithmetic.count_strictMono

Order.RelClasses

Set notation form of le_antisymm

theorem subset_antisymm.{u_1} {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} :
  a ⊆ b → b ⊆ a → a = b

Used by: Topology.isNerveCover_inter

Order.SetNotation

Indexed union of a family of sets

def Set.iUnion.{u, v} {α : Type u} {ι : Sort v} (s : ι → Set α) : Set α

Used by: HeapCover.whole, HeapCover.whole_at, HeapCover.whole_domain, HeapCover.whole_domain_isOpen, Topology.IsNerveCover, Topology.isNerveCover_inter

theorem Set.mem_iUnion.{u, v} {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α} :
  x ∈ ⋃ i, s i ↔ ∃ i, x ∈ s i

Used by: HeapCover.whole, HeapCover.whole_at, Topology.isNerveCover_inter

Order.TypeTags

Attach ⊥ to a type.

def WithBot.{u_2} (α : Type u_2) : Type u_2

Used by: Frame.generator_not_dvd_pow, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any

Order.WellFounded

theorem WellFounded.wellFounded_iff_has_min.{u_1} {α : Type u_1} {r : α → α → Prop} :
  WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m

Used by: Structure.Arithmetic.lt_wf

SetTheory.Cardinal.Finite

Because this theorem takes Fintype α as a non-instance argument, it can be used in particular when Fintype.card ends up with different instance than the one found by inference

theorem Fintype.card_eq_nat_card.{u_1} {α : Type u_1} {x✝ : Fintype α} : Fintype.card α = Nat.card α

Used by: Tower.card_lt_stepNeg, Tower.card_lt_stepPos

Nat.card α is the cardinality of α as a natural number. If α is infinite, Nat.card α = 0.

def Nat.card.{u_3} (α : Type u_3) : ℕ

Used by: Structure.Arithmetic.Tower.instInfiniteColimit, Structure.Arithmetic.Tower.lt_card_level, Tower.card_lt_stepNeg, Tower.card_lt_stepPos, Tower.card_zero_le_neg, Tower.card_zero_le_pos

theorem Nat.card_eq_fintype_card.{u_1} {α : Type u_1} [Fintype α] : Nat.card α = Fintype.card α

Used by: Structure.Arithmetic.Tower.lt_card_level

theorem Nat.card_le_card_of_injective.{u, v} {α : Type u} {β : Type v} [Finite β] (f : α → β)
  (hf : Function.Injective f) : Nat.card α ≤ Nat.card β

Used by: Structure.Arithmetic.Tower.instInfiniteColimit

SetTheory.Cardinal.NatCard

theorem Finite.one_lt_card_iff_nontrivial.{u_1} {α : Type u_1} [Finite α] : 1 < Nat.card α ↔ Nontrivial α

Used by: Structure.Arithmetic.Tower.lt_card_level

Tactic.Linarith.Lemmas

theorem Mathlib.Tactic.Linarith.add_lt_of_le_of_neg.{u} {α : Type u} [Semiring α] [PartialOrder α]
  [IsStrictOrderedRing α] {a b c : α} (hbc : b ≤ c) (ha : a < 0) : b + a < c

Used by: InformationSystem.Step.bottom, InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

theorem Mathlib.Tactic.Linarith.add_lt_of_neg_of_le.{u} {α : Type u} [Semiring α] [PartialOrder α]
  [IsStrictOrderedRing α] {a b c : α} (ha : a < 0) (hbc : b ≤ c) : a + b < c

Used by: Channel.lossy_loses_overall, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.spontaneous_no_self_return

theorem Mathlib.Tactic.Linarith.add_nonpos.{u} {α : Type u} [Semiring α] [PartialOrder α] [IsOrderedRing α]
  {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0

Used by: InformationSystem.zero_run_le

theorem Mathlib.Tactic.Linarith.le_of_eq_of_le.{u} {α : Type u} [Semiring α] [PartialOrder α] {a b : α}
  (ha : a = 0) (hb : b ≤ 0) : a + b ≤ 0

Used by: InformationSystem.Step.bottom, InformationSystem.zero_run_le

theorem Mathlib.Tactic.Linarith.sub_nonpos_of_le.{u} {α : Type u} [Ring α] [PartialOrder α]
  [IsOrderedRing α] {a b : α} : a ≤ b → a - b ≤ 0

Used by: Channel.lossy_loses_overall, InformationSystem.Step.bottom, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

Tactic.LinearCombination.Lemmas

theorem Mathlib.Tactic.LinearCombination.add_eq_eq.{u_1} {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [Add α]
  (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) : a₁ + a₂ = b₁ + b₂

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_set_flip

theorem Mathlib.Tactic.LinearCombination.eq_of_eq.{u_1} {α : Type u_1} {a a' b b' : α} [Add α]
  [IsRightCancelAdd α] (p : a = b) (H : a' + b = b' + a) : a' = b'

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip

Alias of the forward direction of sub_eq_zero.

theorem Mathlib.Tactic.LinearCombination.eq_rearrange.{u_3} {G : Type u_3} [AddGroup G] {a b : G} :
  a - b = 0 → a = b

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip

theorem Mathlib.Tactic.LinearCombination.mul_const_eq.{u_1} {α : Type u_1} {b c : α} [Mul α] (p : b = c)
  (a : α) : a * b = a * c

Used by: Frame.crc_poly_dvd

theorem Mathlib.Tactic.LinearCombination.mul_eq_const.{u_1} {α : Type u_1} {a b : α} [Mul α] (p : a = b)
  (c : α) : a * c = b * c

Used by: Frame.toPoly_set_flip

Tactic.NormNum.Basic

theorem Mathlib.Meta.NormNum.isNat_add.{u_1} {α : Type u_1} [AddMonoidWithOne α] {f : α → α → α} {a b : α}
  {a' b' c : ℕ} :
  f = HAdd.hAdd →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.add b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_set_flip

theorem Mathlib.Meta.NormNum.isNat_eq_true.{u} {α : Type u} [AddMonoidWithOne α] {a b : α} {c : ℕ} :
  Mathlib.Meta.NormNum.IsNat a c → Mathlib.Meta.NormNum.IsNat b c → a = b

Used by: Bit.discrete, Bool.discrete, Unit.discrete, phoneNumberInformation_eq

theorem Mathlib.Meta.NormNum.isNat_mul.{u_1} {α : Type u_1} [Semiring α] {f : α → α → α} {a b : α}
  {a' b' c : ℕ} :
  f = HMul.hMul →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.mul b' = c → Mathlib.Meta.NormNum.IsNat (a * b) c

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, phoneNumberInformation_eq

theorem Mathlib.Meta.NormNum.isNat_natCast.{u_1} {R : Type u_1} [AddMonoidWithOne R] (n m : ℕ) :
  Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m

Used by: Bit.discrete, Bool.discrete, Unit.discrete, phoneNumberInformation_eq

Tactic.NormNum.Eq

theorem Mathlib.Meta.NormNum.isNat_eq_false.{u_1} {α : Type u_1} [AddMonoidWithOne α] [CharZero α] {a b : α}
  {a' b' : ℕ} :
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.beq b' = false → ¬a = b

Used by: irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation

Tactic.NormNum.Ineq

theorem Mathlib.Meta.NormNum.isNat_le_true.{u_1} {α : Type u_1} [Semiring α] [PartialOrder α]
  [IsOrderedRing α] {a b : α} {a' b' : ℕ} :
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.ble b' = true → a ≤ b

Used by: instNormNonnegBit, instNormNonnegCell, irrational_logb_two_five, irrational_logb_two_three, phoneNumber_bits_needed

theorem Mathlib.Meta.NormNum.isNat_lt_true.{u_1} {α : Type u_1} [Semiring α] [PartialOrder α]
  [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ} :
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.ble a' = false → a < b

Used by: irrational_logb_two_five, irrational_logb_two_three, phoneNumberInformation_eq, phoneNumber_bits_needed

Tactic.NormNum.Pow

theorem Mathlib.Meta.NormNum.IsNatPowT.bit0 {a b c : ℕ} :
  Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b) (c.mul c)

Used by: phoneNumber_bits_needed

theorem Mathlib.Meta.NormNum.IsNatPowT.bit1 {a b c : ℕ} :
  Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b + 1) (c.mul (c.mul a))

Used by: phoneNumberInformation_eq, phoneNumber_bits_needed

theorem Mathlib.Meta.NormNum.IsNatPowT.run {a b c : ℕ}
  (p : Mathlib.Meta.NormNum.IsNatPowT (a.pow 1 = a) a b c) : a.pow b = c

Used by: phoneNumberInformation_eq, phoneNumber_bits_needed

This is the key to making the proof proceed as a balanced tree of applications instead of a linear sequence. It is just modus ponens after unwrapping the definitions.

theorem Mathlib.Meta.NormNum.IsNatPowT.trans {a b c : ℕ} {p : Prop} {b' c' : ℕ}
  (h1 : Mathlib.Meta.NormNum.IsNatPowT p a b c)
  (h2 : Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a b' c') :
  Mathlib.Meta.NormNum.IsNatPowT p a b' c'

Used by: phoneNumberInformation_eq, phoneNumber_bits_needed

theorem Mathlib.Meta.NormNum.isNat_pow.{u_1} {α : Type u_1} [Semiring α] {f : α → ℕ → α} {a : α}
  {b a' b' c : ℕ} :
  f = HPow.hPow →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.pow b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c

Used by: phoneNumberInformation_eq, phoneNumber_bits_needed

Tactic.NormNum.Result

A “raw int cast” is an expression of the form:

  • (Nat.rawCast lit : α) where lit is a raw natural number literal
  • (Int.rawCast (Int.negOfNat lit) : α) where lit is a nonzero raw natural number literal

(That is, we only actually use this function for negative integers.) This representation is used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

def Int.rawCast.{u} {α : Type u} [Ring α] (n : ℤ) : α

Used by: Channel.lossless_stationary, Channel.lossy_loses_overall, Component.Simplex.toInformationSystem, Component.parallel, Component.sequential, Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, InformationSystem.Environment.universe, InformationSystem.Step.bottom, InformationSystem.Step.delta_alt, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.eval_delta, InformationSystem.parallel_delta, InformationSystem.roundtrip_neutral, InformationSystem.spontaneous_no_self_return, InformationSystem.toSimplex, InformationSystem.zero_run_le, Topology.step_conserves, irrational_logb_two_five, irrational_logb_two_three

theorem Mathlib.Meta.NormNum.IsNat.raw_refl (n : ℕ) : Mathlib.Meta.NormNum.IsNat n n

Used by: irrational_phoneNumberInformation

A shortcut (non)instance for Nat.AtLeastTwo (n + 2) to shrink generated proofs.

theorem Mathlib.Meta.NormNum.instAtLeastTwo (n : ℕ) : (n + 2).AtLeastTwo

Used by: instNormNonnegCell, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, phoneNumberInformation_eq

Tactic.Positivity.Core

theorem Mathlib.Meta.Positivity.pos_of_isNat.{u_1} {A : Type u_1} {e : A} {n : ℕ} [Semiring A]
  [PartialOrder A] [IsOrderedRing A] [Nontrivial A] (h : Mathlib.Meta.NormNum.IsNat e n)
  (w : Nat.ble 1 n = true) : 0 < e

Used by: phoneNumberInformation_eq

Tactic.Push

theorem Mathlib.Tactic.Push.not_and_eq (p q : Prop) : (¬(p ∧ q)) = (p → ¬q)

Used by: BitFunction.exists_settle

Tactic.Ring.Basic

theorem Mathlib.Tactic.Ring.cast_pos.{u_1} {R : Type u_1} [CommSemiring R] {a : R} {n : ℕ} :
  Mathlib.Meta.NormNum.IsNat a n → a = n.rawCast + 0

Used by: Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_append, Frame.toPoly_set_flip, Topology.step_conserves, irrational_phoneNumberInformation, phoneNumberInformation_eq

Tactic.Ring.Common

theorem Mathlib.Tactic.Ring.Common.add_mul.{u_1} {R : Type u_1} [CommSemiring R] {a₁ a₂ b c₁ c₂ d : R} :
  a₁ * b = c₁ → a₂ * b = c₂ → c₁ + c₂ = d → (a₁ + a₂) * b = d

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, phoneNumberInformation_eq

theorem Mathlib.Tactic.Ring.Common.add_overlap_pf.{u_1} {R : Type u_1} [CommSemiring R] {a b c : R} (x : R)
  (e : ℕ) (pq_pf : a + b = c) : x ^ e * a + x ^ e * b = x ^ e * c

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_set_flip

theorem Mathlib.Tactic.Ring.Common.add_pf_add_overlap.{u_1} {R : Type u_1} [CommSemiring R]
  {a₁ a₂ b₁ b₂ c₁ c₂ : R} : a₁ + b₁ = c₁ → a₂ + b₂ = c₂ → a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_set_flip

theorem Mathlib.Tactic.Ring.Common.mul_add.{u_1} {R : Type u_1} [CommSemiring R] {a b₁ b₂ c₁ c₂ d : R} :
  a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, phoneNumberInformation_eq

theorem Mathlib.Tactic.Ring.Common.mul_congr.{u_1} {R : Type u_1} [CommSemiring R] {a a' b b' c : R} :
  a = a' → b = b' → a' * b' = c → a * b = c

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly_append, Frame.toPoly_set_flip, Frame.toPoly_xor, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, phoneNumberInformation_eq

theorem Mathlib.Tactic.Ring.Common.mul_pf_left.{u_1} {R : Type u_1} [CommSemiring R] {a₃ b c : R} (a₁ : R)
  (a₂ : ℕ) : a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation

theorem Mathlib.Tactic.Ring.Common.mul_pf_right.{u_1} {R : Type u_1} [CommSemiring R] {a b₃ c : R} (b₁ : R)
  (b₂ : ℕ) : a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor, irrational_logb_two_five, irrational_logb_two_three, irrational_phoneNumberInformation, phoneNumberInformation_eq

theorem Mathlib.Tactic.Ring.Common.mul_pow_mul.{u_1} {R : Type u_1} [CommSemiring R] {a₂ c₂ : R}
  {ea₁ b c₁ : ℕ} {xa₁ c₃ d : R} :
  ea₁ * b = c₁ →
    a₂ ^ b = c₂ → xa₁ ^ c₁ * Nat.rawCast 1 = c₃ → c₃ * c₂ = d → (xa₁ ^ ea₁ * a₂) ^ b = d

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor

theorem Mathlib.Tactic.Ring.Common.one_pow.{u_1} {R : Type u_1} [CommSemiring R] {a : R} (b : ℕ)
  (ha : Mathlib.Meta.NormNum.IsNat a 1) : a ^ b = a

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor

theorem Mathlib.Tactic.Ring.Common.pow_add.{u_1} {R : Type u_1} [CommSemiring R] {a c₁ c₂ : R} {b₁ b₂ : ℕ}
  {d : R} : a ^ b₁ = c₁ → a ^ b₂ = c₂ → c₁ * c₂ = d → a ^ (b₁ + b₂) = d

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor

theorem Mathlib.Tactic.Ring.Common.pow_congr.{u_1} {R : Type u_1} [CommSemiring R] {a a' c : R} {b b' : ℕ} :
  a = a' → b = b' → a' ^ b' = c → a ^ b = c

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor

theorem Mathlib.Tactic.Ring.Common.pow_one_cast_of_isNat.{u_1} {R : Type u_1} [CommSemiring R] (a : R)
  (b : ℕ) (hb : Mathlib.Meta.NormNum.IsNat b 1) : a ^ b = a

Used by: Frame.crc_poly_dvd, Frame.toPoly_append

theorem Mathlib.Tactic.Ring.Common.pow_zero.{u_1} {R : Type u_1} [CommSemiring R] (a : R) {e : R}
  (h : Nat.rawCast 1 = e) : a ^ 0 = e + 0

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor

theorem Mathlib.Tactic.Ring.Common.single_pow.{u_1} {R : Type u_1} [CommSemiring R] {a c : R} {b : ℕ} :
  a ^ b = c → (a + 0) ^ b = c + 0

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.generator_not_dvd_pow, Frame.toPoly_append, Frame.toPoly_ne_zero_of_any, Frame.toPoly_set_flip, Frame.toPoly_xor

Topology.Basic

theorem isOpen_iUnion.{u, v} {X : Type u} {ι : Sort v} [TopologicalSpace X] {f : ι → Set X}
  (h : ∀ (i : ι), IsOpen (f i)) : IsOpen (⋃ i, f i)

Used by: HeapCover.whole_domain_isOpen

Topology.Defs.Basic

IsOpen s means that s is open in the ambient topological space on X

def IsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop

Used by: HeapCover.whole_domain_isOpen

Topology.Sets.Opens

The type of open subsets of a topological space.

structure TopologicalSpace.Opens.{u_2} (α : Type u_2) [TopologicalSpace α] : Type u_2

Used by: Heap.grothendieckTopology, Tower.grothendieckTopology