Commit 2023-01-14 04:05 ea3b08cb

View on Github →

feat: port Logic.Encodable.Basic (#1517) Port of logic.encodable.basic

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Encodable/Basic.lean

added theorem Directed.le_sequence

added theorem Directed.rel_sequence

added theorem Directed.sequence_mono

added theorem Directed.sequence_mono_nat

added theorem Encodable.Subtype.encode_eq

added def Encodable.Unique.encodable

added theorem Encodable.axiom_of_choice

added def Encodable.choose

added def Encodable.chooseX

added theorem Encodable.choose_spec

added def Encodable.decidableEqOfEncodable

added def Encodable.decidableRangeEncode

added def Encodable.decodeSigma

added def Encodable.decodeSubtype

added def Encodable.decodeSum

added theorem Encodable.decode_ge_two

added theorem Encodable.decode_nat

added theorem Encodable.decode_ofEquiv

added theorem Encodable.decode_one

added theorem Encodable.decode_option_succ

added theorem Encodable.decode_option_zero

added theorem Encodable.decode_prod_val

added theorem Encodable.decode_sigma_val

added theorem Encodable.decode_sum_val

added theorem Encodable.decode_unit_succ

added theorem Encodable.decode_unit_zero

added theorem Encodable.decode_zero

added def Encodable.decode₂

added theorem Encodable.decode₂_encode

added theorem Encodable.decode₂_eq_some

added theorem Encodable.decode₂_inj

added theorem Encodable.decode₂_is_partial_inv

added theorem Encodable.decode₂_ne_none_iff

added def Encodable.encode'

added def Encodable.encodeSigma

added def Encodable.encodeSubtype

added def Encodable.encodeSum

added theorem Encodable.encode_false

added theorem Encodable.encode_inj

added theorem Encodable.encode_injective

added theorem Encodable.encode_inl

added theorem Encodable.encode_inr

added theorem Encodable.encode_nat

added theorem Encodable.encode_none

added theorem Encodable.encode_ofEquiv

added theorem Encodable.encode_prod_val

added theorem Encodable.encode_sigma_val

added theorem Encodable.encode_some

added theorem Encodable.encode_star

added theorem Encodable.encode_true

added theorem Encodable.encodek₂

added def Encodable.equivRangeEncode

added theorem Encodable.mem_decode₂'

added theorem Encodable.mem_decode₂

added theorem Encodable.nonempty_encodable

added def Encodable.ofEquiv

added def Encodable.ofLeftInjection

added def Encodable.ofLeftInverse

added theorem Encodable.skolem

added theorem Encodable.surjective_decode_iget

added def Quotient.rep

added theorem Quotient.rep_spec

added def Ulower.down

added theorem Ulower.down_eq_down

added theorem Ulower.down_up

added def Ulower.equiv

added def Ulower.up

added theorem Ulower.up_down

added theorem Ulower.up_eq_up

added def Ulower

added def encodableQuotient

added theorem nonempty_encodable